English
The canonical inclusion of rings R →+* Unitization(R, A) is defined by inl, preserving 1 and multiplication.
Русский
Каноническое включение колец R →+* Unitization(R, A) задаётся через inl, сохраняющее 1 и умножение.
LaTeX
$$$\mathrm{inlRingHom}: R \to\!+*\mathrm{Unitization}(R,A)\quad\text{with } \mathrm{map\_one'}=\mathrm{inl\_one},\ \mathrm{map\_mul'}=\mathrm{inl\_mul},\ \mathrm{map\_zero'}=\mathrm{inl\_zero},\ \mathrm{map\_add'}=\mathrm{inl\_add}.$$$
Lean4
/-- The canonical inclusion of rings `R →+* Unitization R A`. -/
@[simps apply]
def inlRingHom [Semiring R] [NonUnitalSemiring A] [Module R A] : R →+* Unitization R A
where
toFun := inl
map_one' := inl_one A
map_mul' := inl_mul A
map_zero' := inl_zero A
map_add' := inl_add A
