lambda_sq_dvd_c — Mathlib

English

In the three-gen framework, S'.multiplicity is at least 2.

Русский

В рамках трёхгенераторов кратность S' не менее 2.

LaTeX

$$$2 \le S'.multiplicity$$$

Lean4

/-- Given `S' : Solution'`, we have that `λ ^ 2` divides `S'.c`. -/
theorem lambda_sq_dvd_c : λ ^ 2 ∣ S'.c :=
  by
  have hm := S'.multiplicity_lambda_c_finite
  suffices 2 ≤ multiplicity (hζ.toInteger - 1) S'.c
    by
    obtain ⟨x, hx⟩ := pow_multiplicity_dvd (hζ.toInteger - 1) S'.c
    refine ⟨λ ^ (multiplicity (hζ.toInteger - 1) S'.c - 2) * x, ?_⟩
    rw [← mul_assoc, ← pow_add]
    convert hx using 3
    simp [this]
  have := lambda_pow_four_dvd_c_cube S'
  rw [pow_dvd_iff_le_emultiplicity, emultiplicity_pow hζ.zeta_sub_one_prime', hm.emultiplicity_eq_multiplicity] at this
  norm_cast at this
  cutsat

Похожие утверждения