addMonoidHom

Mathlib.Algebra.Group.Finsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.embDomain.addMonoidHom

Lean4

/-- Bundle `Finsupp.embDomain f` as an additive map from `ι →₀ M` to `F →₀ M`. -/
@[simps]
def addMonoidHom (f : ι ↪ F) : (ι →₀ M) →+ F →₀ M
    where
  toFun v := embDomain f v
  map_zero' := by simp
  map_add' v
    w := by
    ext b
    by_cases h : b ∈ Set.range f
    · rcases h with ⟨a, rfl⟩
      simp
    · simp only [coe_add, Pi.add_apply, embDomain_notin_range _ _ _ h, add_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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