ideal_eq_span_pow_irreducible — Mathlib

English

If s is a nonzero ideal and ϖ is irreducible, then s equals the span of ϖ^n for some n.

Русский

Если s непрямой идеал и ϖ ирредуцируем, то s равно порожденному элементу ϖ^n.

LaTeX

$$$\exists n \in \mathbb{N},\ s = \langle ϖ^n \rangle$$$

Lean4

theorem ideal_eq_span_pow_irreducible {s : Ideal R} (hs : s ≠ ⊥) {ϖ : R} (hirr : Irreducible ϖ) :
    ∃ n : ℕ, s = Ideal.span {ϖ ^ n} :=
  by
  have gen_ne_zero : generator s ≠ 0 := by
    rw [Ne, ← eq_bot_iff_generator_eq_zero]
    assumption
  rcases associated_pow_irreducible gen_ne_zero hirr with ⟨n, u, hnu⟩
  use n
  have : span _ = _ := Ideal.span_singleton_generator s
  rw [← this, ← hnu, span_singleton_eq_span_singleton]
  use u

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