Theorems · Definition · commutative algebra

Ideal.Quotient.field

{R : Type u_5} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I)

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].

Defined in

Mathlib.RingTheory.Ideal.Quotient.Basic

Cited by

25 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIdeal.IsMaximal