map_id

Mathlib.Algebra.Group.Units.Hom

URI: https://scilib.ai/kg/mathlib#Units.map_id

English

The map induced by the identity MonoidHom is the identity on Units M.

Русский

Отображение, индуцируемое единичным гомоморфизмом Monoid, является тождественным на единицах M.

LaTeX

$$$\\mathrm{map}(\\mathrm{MonoidHom.id}\\;M) = \\mathrm{MonoidHom.id}\\;Mˣ$$$

Lean4

@[to_additive (attr := simp)]
theorem map_id : map (MonoidHom.id M) = MonoidHom.id Mˣ := by ext; rfl

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

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

Разделы

Аффилиация

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