English
Constructs a DivisionRing structure on a ring with the property that every element is a unit or zero; internal lemmas ensure compatibility of operations.
Русский
Строит структуру DivisionRing на кольце, если каждый элемент либо единица-обратимый, либо ноль; обеспечиваются совместимости операций.
LaTeX
$$$\\text{DivisionRing } R \\text{ from } \\forall a \\in R, \\text{IsUnit}(a) \\lor a = 0$$$
Lean4
/-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0. -/
-- See note [reducible non-instances]
noncomputable abbrev ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) : Field R
where
toCommRing := ‹CommRing R›
__ := DivisionRing.ofIsUnitOrEqZero h
