inclusion_self

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#SubgroupClass.inclusion_self

English

The inclusion map on an object is the identity when viewed as an element of H.

Русский

Включение на элементе равно идентичности в терминах H.

LaTeX

$$$$ inclusion(le\\_rfl) x = x. $$$$

Lean4

@[to_additive (attr := simp)]
theorem inclusion_self (x : H) : inclusion le_rfl x = x :=
  by
  cases x
  rfl

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

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

Разделы

Аффилиация

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