English
If the action of R on S is compatible with multiplication on S and S is a scalar tower over R, then the map r ↦ r • 1 is a ring homomorphism R →+* S.
Русский
Если действие R на S совместимо с умножением в S и S образует скалярную башню над R, то отображение r ↦ r • 1 является кольцевым гомоморфизмом R →+* S.
LaTeX
$$$\\text{smulOneHom} : R \\to+* S, \\; r \\mapsto r \\cdot 1_S$$$
Lean4
/-- If the module action of `R` on `S` is compatible with multiplication on `S`, then
`fun x ↦ x • 1` is a ring homomorphism from `R` to `S`.
This is the `RingHom` version of `MonoidHom.smulOneHom`.
When `R` is commutative, usually `algebraMap` should be preferred. -/
@[simps!]
def smulOneHom [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S
where
__ := MonoidHom.smulOneHom
map_zero' := zero_smul R 1
map_add' := (add_smul · · 1)
