associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b

English

The multiplicity of the descended solution is strictly less by 1: (S.Solution'_descent).multiplicity = S.multiplicity - 1.

Русский

Кратность нисхождения меньше на единицу: S.Solution'_descent.multiplicity = S.multiplicity - 1.

LaTeX

$$S.Solution'_descent.multiplicity = S.multiplicity - 1$$

Lean4

/-- If `p : 𝓞 K` is a prime that divides both `S.a + S.b` and `S.a + η * S.b`, then `p`
is associated with `λ`. -/
theorem associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b {p : 𝓞 K} (hp : Prime p) (hpab : p ∣ S.a + S.b)
    (hpaηb : p ∣ S.a + η * S.b) : Associated p λ :=
  by
  suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
  rw [← one_mul S.a, ← one_mul S.b] at hpab
  rw [← one_mul S.a] at hpaηb
  have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηb
  rwa [one_mul, one_mul, coe_eta, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this

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