associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b

English

The square λ^2 does not divide S.a + η^2 S.b.

Русский

Квадрат λ^2 не делит S.a + η^2 S.b.

LaTeX

$$Not (λ^2 ∣ S.a + η^2 S.b)$$

Lean4

/-- If `p : 𝓞 K` is a prime that divides both `S.a + S.b` and `S.a + η ^ 2 * S.b`, then `p`
is associated with `λ`. -/
theorem associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b {p : 𝓞 K} (hp : Prime p) (hpab : p ∣ (S.a + S.b))
    (hpaηsqb : p ∣ (S.a + η ^ 2 * 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ηsqb
  have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηsqb
  rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime, ← dvd_neg] at this
  convert dvd_mul_of_dvd_left this η using 1
  rw [eta_sq, neg_sub, sub_mul, sub_mul, neg_mul, ← pow_two, eta_sq, coe_eta]
  ring

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