comp_smul_left — Mathlib

English

The composition of left smuls corresponds to the product of scalars: (a1 • ·) ∘ (a2 • ·) = ((a1*a2) • ·).

Русский

Сложение левых скаляров соответствует произведению скаляров: (a1 • ·) ∘ (a2 • ·) = ((a1*a2) • ·).

LaTeX

$$$\\\\forall a_1,a_2 \\\\in M, \\\\ (a_1 \\\\cdot ·) \\\\circ (a_2 \\\\cdot ·) = (((a_1 \\\\cdot a_2) \\\\cdot ·) : α \\\\to α).$$$

Lean4

/-- `SMul` version of `comp_mul_left` -/
@[to_additive /-- `VAdd` version of `comp_add_left` -/
    ]
theorem comp_smul_left (a₁ a₂ : M) : (a₁ • ·) ∘ (a₂ • ·) = (((a₁ * a₂) • ·) : α → α) :=
  funext fun _ ↦ (mul_smul _ _ _).symm

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