relIndex_toSubgroup — Mathlib

English

The relative index for AddSubgroup coincides with the relative index for the original subgroups: AddSubgroup.toSubgroup H and AddSubgroup.toSubgroup K have the same relIndex as H and K.

Русский

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

LaTeX

$$AddSubgroup.relIndex_toSubgroup = ...$$

Lean4

@[simp]
theorem _root_.AddSubgroup.relIndex_toSubgroup {G : Type*} [AddGroup G] (H K : AddSubgroup G) :
    (AddSubgroup.toSubgroup H).relIndex (AddSubgroup.toSubgroup K) = H.relIndex K :=
  rfl

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