ideal_span_absNorm_eq_self — Mathlib

English

In a principal ideal ring, every ideal J ⊆ Z satisfies span{absNorm(J)} = J.

Русский

В главном кольце идеалов каждый идеал J ⊆ Z удовлетворяет равенству span{absNorm(J)} = J.

LaTeX

$$$$\text{If } J\subseteq \mathbb{Z} \text{ is an ideal, then } \operatorname{span}\{|\operatorname{absNorm}(J)|\} = J.$$$$

Lean4

@[simp]
theorem ideal_span_absNorm_eq_self (J : Ideal ℤ) : span {(absNorm J : ℤ)} = J :=
  by
  obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J
  simp

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