toAddMonoidAlgebra_mul — Mathlib

English

Multiplication is preserved by the toAddMonoidAlgebra map: the image of the product equals the product of images.

Русский

Отображение toAddMonoidAlgebra сохраняет умножение: образ произведения равен произведению образов.

LaTeX

$$$ (f * g).toAddMonoidAlgebra = toAddMonoidAlgebra f * toAddMonoidAlgebra g $$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_mul [AddMonoid ι] [Semiring M] [∀ m : M, Decidable (m ≠ 0)] (f g : ⨁ _ : ι, M) :
    (f * g).toAddMonoidAlgebra = toAddMonoidAlgebra f * toAddMonoidAlgebra g :=
  by
  apply_fun AddMonoidAlgebra.toDirectSum
  · simp
  · apply Function.LeftInverse.injective
    apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

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