ideal_eq_span_pow_p — Mathlib

English

Every nonzero ideal s of ℤ_p is a principal ideal generated by p^n for some n.

Русский

Каждый ненулевой идеал s в ℤ_p является порожденным p^n для некоторого n.

LaTeX

$$∀ s ≠ ⊥, ∃ n, s = (p : ℤ_[p])^n ℤ_[p].$$

Lean4

theorem ideal_eq_span_pow_p {s : Ideal ℤ_[p]} (hs : s ≠ ⊥) : ∃ n : ℕ, s = Ideal.span {(p : ℤ_[p]) ^ n} :=
  IsDiscreteValuationRing.ideal_eq_span_pow_irreducible hs irreducible_p

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