associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b

English

There exists a Solution with multiplicity strictly smaller than that of the given S.

Русский

Существует решение с кратностью строго меньше заданного S.

LaTeX

$$∃ S₁ : Solution hζ, S₁.multiplicity < S.multiplicity$$

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_eta_mul_b_of_dvd_a_add_eta_sq_mul_b {p : 𝓞 K} (hp : Prime p) (hpaηb : 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] at hpaηb
  rw [← one_mul S.a] at hpaηsqb
  have := dvd_mul_sub_mul_mul_gcd_of_dvd hpaηb hpaηsqb
  rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this
  convert (dvd_mul_of_dvd_left (dvd_mul_of_dvd_left this η) η) using 1
  symm
  calc
    _ = (-η.1 - 1 - η) * (-η - 1) := by rw [eta_sq, mul_assoc, ← pow_two, eta_sq]
    _ = 2 * η.1 ^ 2 + 3 * η + 1 := by ring
    _ = λ := by rw [eta_sq, coe_eta]; ring

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