relIndex_bot_left

Mathlib.GroupTheory.Index

URI: https://scilib.ai/kg/mathlib#Subgroup.relIndex_bot_left

English

The left relative index of the bottom subgroup with respect to H equals Nat.card H.

Русский

Левый относительный индекс нулевой подгруппы относительно H равен натуральному отношению к H.

LaTeX

$$$ (\bot_G).relIndex(H) = |H|. $$$

Lean4

@[to_additive (attr := simp)]
theorem relIndex_bot_left : (⊥ : Subgroup G).relIndex H = Nat.card H := by rw [relIndex, bot_subgroupOf, index_bot]

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

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

Разделы

Аффилиация

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