irreducible_iff_uniformizer — Mathlib

English

If an irreducible element is given, then the maximal ideal equals the span of that element.

Русский

Если дан элемент irreducible, то максимальный идеал равен породе его порожденной.

LaTeX

$$$\forall (R) [\mathrm{CommRing R}] [IsDomain R] [IsDiscreteValuationRing R] (\varpi : R)\; (h : Irreducible \varpi) → IsLocalRing.maximalIdeal R = \mathrm{Ideal}.span\{\varpi\}$$$

Lean4

/-- An element of a DVR is irreducible iff it is a uniformizer, that is, generates the
  maximal ideal of `R`. -/
theorem irreducible_iff_uniformizer (ϖ : R) : Irreducible ϖ ↔ maximalIdeal R = Ideal.span { ϖ } :=
  ⟨fun hϖ => (eq_maximalIdeal (isMaximal_of_irreducible hϖ)).symm, fun h =>
    irreducible_of_span_eq_maximalIdeal ϖ (fun e => not_a_field R <| by rwa [h, span_singleton_eq_bot]) h⟩

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