English
There is a standard way to turn a ring hom i: R →+* S between commutative semirings into an Algebra R S; the construction uses a toAlgebra' with commutativity to provide the Algebra structure.
Русский
Существует стандартный способ превратить гомоморфизм колец i: R →+* S между коммутативными полусистемами в структуру Algebra R S; конструкция использует toAlgebra' с коммутативностью.
LaTeX
$$$\text{RingHom.toAlgebra}(i) : Algebra\ R\ S$$$
Lean4
/-- Creating an algebra from a morphism to a commutative semiring.
See note [reducible non-instances].
*Warning:* In general this should not be used if `S` already has a `SMul R S`
instance, since this creates another `SMul R S` instance from the supplied `RingHom` and
this will likely create a diamond. -/
abbrev toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
i.toAlgebra' fun _ => mul_comm _
