English
If every element of a ring R is either a unit or zero, then R carries a DivisionRing structure.
Русский
Если каждый элемент кольца R либо единица (обратимый) либо ноль, то R можно наделить структурой division ring.
LaTeX
$$$\\forall a \\in R, \\text{IsUnit}(a) \\lor a = 0 \\;\Rightarrow\\; \\exists \\text{DivisionRing } R$$$
Lean4
/-- Constructs a `DivisionRing` structure on a `Ring` consisting only of units and 0. -/
-- See note [reducible non-instances]
noncomputable abbrev ofIsUnitOrEqZero [Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) : DivisionRing R
where
toRing := ‹Ring R›
__ := groupWithZeroOfIsUnitOrEqZero h
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
