refl

Mathlib.GroupTheory.Commensurable

URI: https://scilib.ai/kg/mathlib#Subgroup.Commensurable.refl

English

Any subgroup H of a group G is commensurable with itself: H ~ H.

Русский

Любая подгруппа H группы G комменсурируема с самой собой: H ~ H.

LaTeX

$$Commensurable H H$$

Lean4

@[to_additive (attr := refl)]
protected theorem refl (H : Subgroup G) : Commensurable H H := by simp [Commensurable]

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

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

Разделы

Аффилиация

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