map_one

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#OneHom.map_one

English

A monoid homomorphism sends the unit to the unit: f(1) = 1.

Русский

Гомоморфизм моноидов отправляет единицу в единицу: f(1) = 1.

LaTeX

$$$f(1)=1$$$

Lean4

@[to_additive]
protected theorem map_one [One M] [One N] (f : OneHom M N) : f 1 = 1 :=
  f.map_one'

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

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

Разделы

Аффилиация

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