mul' — Mathlib

English

There is a multiplication map on a non-unital algebra, regarded as an R-linear map mul' : A ⊗_R A → A, sending a ⊗ b to ab.

Русский

Существуют сведение умножения на неединообразной алгебре как линейного отображения над R: mul' : A ⊗_R A → A, где a ⊗ b ↦ ab.

LaTeX

$$$$ mul' : A \otimes_R A \to_R A, \quad mul'(a \otimes b) = ab. $$$$

Lean4

/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/
-- TODO: upgrade to A-linear map if A is a semiring.

def mul' : A ⊗[R] A →ₗ[R] A :=
  TensorProduct.lift (mul R A)

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