toAddMonoidAlgebra_one — Mathlib

English

The direct sum element 1 maps to the multiplicative unit in the AddMonoidAlgebra under the toAddMonoidAlgebra map.

Русский

Элемент единицы в прямой сумме отображается через toAddMonoidAlgebra в единицу умножения в AddMonoidAlgebra.

LaTeX

$$$\bigl(1 : \bigoplus_{i \in \iota} M\bigr).toAddMonoidAlgebra = 1$$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_one [Zero ι] [Semiring M] [∀ m : M, Decidable (m ≠ 0)] :
    (1 : ⨁ _ : ι, M).toAddMonoidAlgebra = 1 :=
  DFinsupp.toFinsupp_single _ _

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