English
The quotient R/I by a maximal ideal I is a division ring, with a multiplicative inverse defined for nonzero elements.
Русский
Фактор-кольцо R/I по максимальному идеалу I является делительским кольцом; для ненулевых элементов существует обратное.
LaTeX
$$DivisionRing (R ⧸ I)$$
Lean4
/-- The quotient by a maximal ideal is a group with zero. This is a `def` rather than `instance`,
since users will have computable inverses in some applications.
See note [reducible non-instances]. -/
protected noncomputable abbrev groupWithZero [hI : I.IsMaximal] : GroupWithZero (R ⧸ I) :=
fast_instance%{
inv := fun a => if ha : a = 0 then 0 else Classical.choose (exists_inv ha)
mul_inv_cancel := fun a (ha : a ≠ 0) =>
show a * dite _ _ _ = _ by rw [dif_neg ha]; exact Classical.choose_spec (exists_inv ha)
inv_zero := dif_pos rfl
__ := Quotient.nontrivial hI.out.1 }
