English
The field structure on the fraction ring is obtained from IsFractionRing isDomain; i.e., every such K becomes a field.
Русский
Поле дробей образуется на основании IsFractionRing isDomain; то есть K становится полем.
LaTeX
$$IsFractionRing.toField$$
Lean4
/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is a field.
See note [reducible non-instances]. -/
@[stacks 09FJ]
noncomputable abbrev toField : Field K where
__ := IsFractionRing.isDomain A
inv := IsFractionRing.inv A
mul_inv_cancel := IsFractionRing.mul_inv_cancel A
inv_zero := show IsFractionRing.inv A (0 : K) = 0 by rw [IsFractionRing.inv]; exact dif_pos rfl
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
