toSemiring_coe_addMonoidHom — Mathlib

English

The induced additive monoid homomorphism from the direct sum to R, obtained from the semiring construction, coincides with the coordinatewise sum from the family.

Русский

Полученный аддитивный моноид-гомоморфизм из прямого сумма в R, полученный через построение полугруппы, совпадает с координатной суммой из семейства.

LaTeX

$$$$(toSemiring f hone hmul) = (toAddMonoid f).$$$$

Lean4

@[simp]
theorem toSemiring_coe_addMonoidHom (f : ∀ i, A i →+ R) (hone hmul) :
    (toSemiring f hone hmul : (⨁ i, A i) →+ R) = toAddMonoid f :=
  rfl

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