relIndex_subgroupOf — Mathlib

English

RelIndex of a subgroup in a larger subgroup equals the relIndex in the smaller context after embedding.

Русский

RelIndex подгруппы внутри большей подгруппы равен relIndex после вложения в меньший контекст.

LaTeX

$$$ (H.\\text{subgroupOf } L).relIndex (K.\\text{subgroupOf } L) = H.relIndex K $$$

Lean4

@[to_additive]
theorem relIndex_subgroupOf (hKL : K ≤ L) : (H.subgroupOf L).relIndex (K.subgroupOf L) = H.relIndex K :=
  ((index_comap (H.subgroupOf L) (inclusion hKL)).trans (congr_arg _ (inclusion_range hKL))).symm

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