relIndex_toAddSubgroup — Mathlib

English

The relative index after passing toAddSubgroup equals the original: (AddSubgroup.toAddSubgroup H).relIndex (AddSubgroup.toAddSubgroup K) = H.relIndex K.

Русский

Относительный индекс после перехода кAddSubgroup равен исходному.

LaTeX

$$ (AddSubgroup.toAddSubgroup H).relIndex (AddSubgroup.toAddSubgroup K) = H.relIndex K$$

Lean4

@[simp]
theorem relIndex_toAddSubgroup : (Subgroup.toAddSubgroup H).relIndex (Subgroup.toAddSubgroup K) = H.relIndex K :=
  rfl

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