map_comp_one

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#map_comp_one

English

For any f in OneHomClass F M N, f ∘ (1) = 1 (as a function).

Русский

Для любого f из OneHomClass F M N выполняется f ∘ 1 = 1 (как функция).

LaTeX

$$$$ f \circ (1 : \iota \to M) = 1. $$$$

Lean4

@[to_additive]
theorem map_comp_one [OneHomClass F M N] (f : F) : f ∘ (1 : ι → M) = 1 := by simp

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

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

Разделы

Аффилиация

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