English
Every ring α carries a canonical Grind.Ring structure compatible with its ring operations.
Русский
Любое кольцо α имеет каноническую структуру Grind.Ring, совместимую с его операциями кольца.
LaTeX
$$$$ \exists r:\text{Grind.Ring}(\alpha). $$$$
Lean4
instance (priority := 100) toGrindRing [s : Ring α] : Grind.Ring α :=
{ s, Semiring.toGrindSemiring α with
nsmul := ⟨s.nsmul⟩
npow := ⟨fun a n => a ^ n⟩
zsmul := ⟨s.zsmul⟩
natCast := inferInstance
intCast := inferInstance
neg_zsmul i a := neg_zsmul a i
neg_add_cancel := by simp [neg_add_cancel]
intCast_ofNat
| 0 => Int.cast_zero
| 1 => Int.cast_one
| _ + 2 => Int.cast_ofNat _
intCast_neg := Int.cast_neg
zsmul_natCast_eq_nsmul n a := natCast_zsmul a n }
