field — Mathlib

English

The quotient of a commutative ring by a maximal ideal is a field.

Русский

Фактор-кольцо коммутативного кольца по максимальному идеалу является полем.

LaTeX

$$$\text{Ideal.Quotient.field } I$$$

Lean4

/-- The quotient of a commutative ring by a maximal ideal is a field.
This is a `def` rather than `instance`, since users
will have computable inverses (and `qsmul`, `ratCast`) in some applications.

See note [reducible non-instances]. -/
protected noncomputable abbrev field {R} [CommRing R] (I : Ideal R) [I.IsMaximal] : Field (R ⧸ I) :=
  fast_instance%{
      __ := commRing _
      __ := Quotient.divisionRing I }

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