inl_mul_inr — Mathlib

English

Left-right multiplication rule: inl(r) * inr(m) = inr(r • m).

Русский

Правило умножения слева и справа: inl(r) * inr(m) = inr(r • m).

LaTeX

$$$(\mathrm{inl}(r) * \mathrm{inr}(m) : \mathrm{tsze}_{R} M) = \mathrm{inr}(r \cdot m)$$$

Lean4

theorem inl_mul_inr [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r : R) (m : M) :
    (inl r * inr m : tsze R M) = inr (r • m) :=
  ext (mul_zero r) <| show r • m + (0 : Rᵐᵒᵖ) • (0 : M) = r • m by rw [smul_zero, add_zero]

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