inr_mul_inl — Mathlib

English

Right-left multiplication rule: inr(m) * inl(r) = inr(m <• r).

Русский

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

LaTeX

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

Lean4

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

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