encard_left

Mathlib.GroupTheory.Complement

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

← MathLib Explorer

English

Again, encard left relates the encoded cardinality of a left complement to the index.

Русский

Снова encard левого комплемента относится к индексу через кардинальное выражение.

LaTeX

$$$\\text{encard}_L(S,H) = \\text{index}_H$$$

Lean4

@[to_additive]
theorem encard_left [H.FiniteIndex] (h : IsComplement S H) : S.encard = H.index := by
  rw [← h.finite_left.cast_ncard_eq, h.ncard_left]

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

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

Разделы

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

Аффилиация

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