inl_smul — Mathlib

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

Похожие утверждения