coe_lmul_eq_mul — Mathlib

English

The underlying function of the left-mmul algebra homomorphism coincides with the standard left-multiplication endomorphism. In other words, for all a ∈ A, the endomorphism corresponding to a is the map x ↦ a x.

Русский

Функция, лежащая в основе гомоморфизма левого умножения, совпадает с обычным эндоморфизмом левым умножением: для каждого a ∈ A отображение, соответствующее a, есть x ↦ a x.

LaTeX

$$$\text{coe }(\mathsf{Algebra.lmul}\ R\ A) = (\lambda a:\, \lambda x:\, a x).$$$

Lean4

@[simp]
theorem _root_.Algebra.coe_lmul_eq_mul : ⇑(Algebra.lmul R A) = mul R A :=
  rfl

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