English
Let S act on R and M with a distributive action. The left injection inl: R → tsze_R M commutes with the S-action: for all s ∈ S and r ∈ R, inl(s · r) = s · inl(r).
Русский
Пусть S действует на кольцо R и модуль M совместно распределимо. Левостороннее вложение inl: R → tsze_R M сохраняет действие S: для любых s ∈ S, r ∈ R выполняется inl(s · r) = s · inl(r).
LaTeX
$$$ (\mathrm{inl}(s \cdot r) : \mathrm{tsze}_{R} M) = s \cdot \mathrm{inl}(r) $$$
Lean4
@[simp]
theorem inl_smul [Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s : S) (r : R) :
(inl (s • r) : tsze R M) = s • inl r :=
ext rfl (smul_zero s).symm