coe_lmul_eq_mul — Mathlib

English

The multiplication in a non-unital algebra defines a bilinear map, expressed via a left-action homomorphism into End_R(A).

Русский

Умножение в неединообразной алгебре задаёт билинейную карту, выражаемую через линейный однородный гомоморфизм в End_R(A).

LaTeX

$$$$ \text{NonUnitalAlgHom.lmul}: A \to_A \text{End}_R(A) \text{ with } map\_mul' = mulLeft\_mul. $$$$

Lean4

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

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