mul_inl_eq_op_smul — Mathlib

English

Right multiplication by inl r equals the smul action on the right: x * inl r = x <• r.

Русский

Правое умножение на inl r равно действию smul справа: x * inl r = x <• r.

LaTeX

$$$x * \mathrm{inl}(r) = x \lhd r$$$

Lean4

theorem mul_inl_eq_op_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M)
    (r : R) : x * inl r = x <• r :=
  ext rfl (by dsimp; rw [smul_zero, zero_add])

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