lambda_dvd_a_add_eta_sq_mul_b — Mathlib

English

If p divides both S.a + S.b and S.a + η^2 S.b, then p is associated with λ.

Русский

Если p делит обе формы S.a + S.b и S.a + η^2 S.b, то p ассоциировано с λ.

LaTeX

$$If p ∣ (S.a + S.b) and p ∣ (S.a + η^2 S.b) then Associated(p, λ).$$

Lean4

/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η ^ 2 * S.b)`. -/
theorem lambda_dvd_a_add_eta_sq_mul_b : λ ∣ (S.a + η ^ 2 * S.b) :=
  by
  rw [show S.a + η ^ 2 * S.b = (S.a + S.b) + λ ^ 2 * S.b + 2 * λ * S.b by rw [coe_eta]; ring]
  exact dvd_add (dvd_add (dvd_trans (dvd_pow_self _ (by decide)) S.hab) ⟨λ * S.b, by ring⟩) ⟨2 * S.b, by ring⟩

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