map'_comp

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.map'_comp

← MathLib Explorer

English

The constructor map' is compatible with composition: map'(g ∘ f) = (map' g) ∘ (map' f).

Русский

Конструктор map' совместим с композициями: map'(g ∘ f) = (map' g) ∘ (map' f).

LaTeX

$$$ map'(g \\circ f) = (map' g) \\circ (map' f) $$$

Lean4

@[simp]
theorem map'_comp (f : α →* β) (g : β →* γ) : map' (g.comp f) = (map' g).comp (map' f) :=
  MonoidWithZeroHom.ext fun x => (map'_map' f g x).symm

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

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

Разделы

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

Аффилиация

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