encard_right

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.IsComplement.encard_right

← MathLib Explorer

English

Similarly for the right encard: encard_right equals the index when H is finite index.

Русский

Аналогично для правого encard: encard_right равно индексу при конечном индексе H.

LaTeX

$$Right encard equality with index under finiteness.$$

Lean4

@[to_additive]
theorem encard_right [H.FiniteIndex] (h : IsComplement H T) : T.encard = H.index := by
  rw [← h.finite_right.cast_ncard_eq, h.ncard_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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