uniqueFactorizationMonoid — Mathlib

English

In a Dedekind domain, the monoid of ideals is a Unique Factorization Monoid: every ideal factors uniquely as a product of prime ideals.

Русский

В детерминированном домене моноид идеалов является уникальным факторизационным моноидом: каждый идеал разлагается уникально в произведение простых идеалов.

LaTeX

$$$\text{UniqueFactorizationMonoid}(\mathrm{Ideal}(A))$$$

Lean4

instance uniqueFactorizationMonoid : UniqueFactorizationMonoid (Ideal A) :=
  {
    irreducible_iff_prime := by
      intro P
      exact
        ⟨fun hirr =>
          ⟨hirr.ne_zero, hirr.not_isUnit, fun I J =>
            by
            have : P.IsMaximal := by
              refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
              intro J hJ
              obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
              exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
            rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def, SetLike.le_def]
            contrapose!
            rintro ⟨⟨x, x_mem, x_notMem⟩, ⟨y, y_mem, y_notMem⟩⟩
            exact ⟨x * y, Ideal.mul_mem_mul x_mem y_mem, mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩⟩,
          Prime.irreducible⟩ }

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