divisionRing — Mathlib

English

For a maximal ideal I in a commutative ring R, the quotient R/I carries a division ring structure.

Русский

Для максимального идеала I в коммутативном кольце R фактор-кольцо R/I имеет структуру делительного кольца.

LaTeX

$$DivisionRing (R ⧸ I)$$

Lean4

/-- 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]. -/
protected noncomputable abbrev divisionRing [I.IsMaximal] : DivisionRing (R ⧸ I) :=
  fast_instance%{
      __ := ring _
      __ := Quotient.groupWithZero _
      nnqsmul := _
      nnqsmul_def _ _ := rfl
      qsmul := _
      qsmul_def _ _ := rfl }

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