Theorems · Definition · commutative algebra

Ideal.Quotient.divisionRing

{R : Type u_3} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → [I.IsMaximal] → DivisionRing (R ⧸ I)

The quotient by a two-sided ideal that is maximal as a left ideal is a division ring. 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

1 results in Mathlib

Foundations

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

Assumes

RingIdeal.IsTwoSidedIdeal.IsMaximal