maximalIdeal_eq_span_p — Mathlib

English

The maximal ideal of Z_p is the principal ideal generated by p.

Русский

Максимальный идеал Z_p равен порожденному p идеалу.

LaTeX

$$MaximalIdeal(ℤ_[p]) = Ideal.span{p}.$$

Lean4

theorem maximalIdeal_eq_span_p : maximalIdeal ℤ_[p] = Ideal.span {(p : ℤ_[p])} :=
  by
  apply le_antisymm
  · intro x hx
    simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits] at hx
    rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
  · rw [Ideal.span_le, Set.singleton_subset_iff]
    exact p_nonunit

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