English
A semiring that is an algebra over a commutative ring carries a natural ring structure on its additive group.
Русский
Полупризерная полугруппа, являющаяся алгеброй над коммутативным кольцом, имеет естественную кольцевую структуру на своей аддитивной группе.
LaTeX
$$abbrev semiringToRing (R) [CommRing R] [Semiring A] [Algebra R A] : Ring A$$
Lean4
/-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.
See note [reducible non-instances]. -/
abbrev semiringToRing (R : Type*) [CommRing R] [Semiring A] [Algebra R A] : Ring A :=
{ __ := (inferInstance : Semiring A)
__ := Module.addCommMonoidToAddCommGroup R
intCast := fun z => algebraMap R A z
intCast_ofNat := fun z => by simp only [Int.cast_natCast, map_natCast]
intCast_negSucc := fun z => by simp }
