count_associates_eq — Mathlib

English

Variant of count_normalizedFactors_eq for associated ideals, equating counts of irreducible factors after mapping through Associates.

Русский

Вариант count_normalizedFactors_eq для связанных идеалов: равенство счётчиков после отображения через Associates.

LaTeX

$$count_associates_eq$$

Lean4

/-- Variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals. -/
theorem count_associates_eq [DecidableEq (Associates (Ideal R))]
    [∀ (p : Associates <| Ideal R), Decidable (Irreducible p)] {a a₀ x : R} {n : ℕ} (hx : Prime x) (ha : ¬x ∣ a)
    (heq : a₀ = x ^ n * a) : (Associates.mk (span { x })).count (Associates.mk (span { a₀ })).factors = n :=
  by
  have hx0 : x ≠ 0 := Prime.ne_zero hx
  classical
  rw [count_associates_factors_eq, UniqueFactorizationMonoid.count_normalizedFactors_eq]
  · exact (prime_span_singleton_iff.mpr hx).irreducible
  · exact normalize_eq _
  · simp only [span_singleton_pow, heq, dvd_span_singleton]
    exact Ideal.mul_mem_right _ _ (mem_span_singleton_self (x ^ n))
  · simp only [span_singleton_pow, heq, dvd_span_singleton, mem_span_singleton]
    rw [pow_add, pow_one, mul_dvd_mul_iff_left (pow_ne_zero n hx0)]
    exact ha
  · simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot]
    aesop
  · exact (span_singleton_prime hx0).mpr hx
  · simp only [ne_eq, span_singleton_eq_bot]; exact hx0

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