comp

Mathlib.Algebra.AddConstMap.Basic

URI: https://scilib.ai/kg/mathlib#AddConstMap.comp

Lean4

/-- Composition of two `AddConstMap`s. -/
@[simps -fullyApplied]
def comp {K : Type*} [Add K] {c : K} (g : H →+c[b, c] K) (f : G →+c[a, b] H) : G →+c[a, c] K :=
  ⟨g ∘ f, by simp⟩

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

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

Разделы

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

Аффилиация

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