irreducible_of_irreducible_absNorm

English

If the absolute norm of I is irreducible in the natural numbers, then I is irreducible as an ideal.

Русский

Если absNorm(I) иррадицирован как простое число, то I ирредуцируем как идеал.

LaTeX

$$Irreducible(absNorm(I)) ⇒ Irreducible(I)$$

Lean4

theorem irreducible_of_irreducible_absNorm {I : Ideal S} (hI : Irreducible (Ideal.absNorm I)) : Irreducible I :=
  irreducible_iff.mpr
    ⟨fun h => hI.not_isUnit (by simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h),
      by
      rintro a b rfl
      simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using hI.isUnit_or_isUnit (map_mul absNorm a b)⟩

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