inl_mul_eq_smul — Mathlib

English

Left multiplication by inl r equals smul by r on the whole element: inl r * x = r • x.

Русский

Умножение слева через inl r эквивалентно действию smul на весь элемент: inl r * x = r • x.

LaTeX

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

Lean4

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

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