lambda_dvd_a_add_eta_mul_b — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η * S.b)`. -/
theorem lambda_dvd_a_add_eta_mul_b : λ ∣ (S.a + η * S.b) :=
  a_add_eta_mul_b S ▸ dvd_add (dvd_trans (dvd_pow_self _ (by decide)) S.hab) ⟨S.b, by rw [mul_comm]⟩

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