fieldOfSubtypeIsMaximal — Mathlib

English

A temporary field structure on the quotients by maximal ideals is provided: for each maximal ideal I, R/I is a field.

Русский

Для каждого максимального идеала I дано поле: R/I является полем.

LaTeX

$$$\forall I \in \mathrm{MaximalSpectrum}(R),\ \mathrm{Field}(R / I)$$$

Lean4

/-- A temporary field instance on the quotients by maximal ideals. -/
@[local instance]
noncomputable def fieldOfSubtypeIsMaximal (I : MaximalSpectrum R) : Field (R ⧸ I.asIdeal) :=
  Ideal.Quotient.field I.asIdeal

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