index_antitone

Mathlib.GroupTheory.Index

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

← MathLib Explorer

English

If H ≤ K, then the index [G:K] ≤ [G:H].

Русский

Если H ⊆ K, то [G:K] ≤ [G:H].

LaTeX

$$K.index ≤ H.index$$

Lean4

@[to_additive (attr := gcongr)]
theorem index_antitone (h : H ≤ K) [H.FiniteIndex] : K.index ≤ H.index :=
  Nat.le_of_dvd (Nat.zero_lt_of_ne_zero FiniteIndex.index_ne_zero) (index_dvd_of_le h)

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

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

Разделы

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

Аффилиация

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