toAddMonoid_of

Mathlib.Algebra.DirectSum.Basic

URI: https://scilib.ai/kg/mathlib#DirectSum.toAddMonoid_of

English

Injectivity of the map toAddMonoid: if toAddMonoid f = toAddMonoid g, then f = g.

Русский

Инъективность отображения toAddMonoid: если toAddMonoid f = toAddMonoid g, то f = g.

LaTeX

$$toAddMonoid_injective$$

Lean4

@[simp]
theorem toAddMonoid_of (i) (x : β i) : toAddMonoid φ (of β i x) = φ i x :=
  DFinsupp.liftAddHom_apply_single φ i x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru