relIndex_pointwise_smul — Mathlib

English

Conjugating both subgroups J and K by h ∈ H leaves their relative index unchanged: (h • J).relIndex (h • K) = J.relIndex K.

Русский

Сопряжение обеих подпогрупп J и K элементом h сохраняет их относительный индекс: (h • J).relIndex (h • K) = J.relIndex K.

LaTeX

$$((h • J).relIndex (h • K)) = J.relIndex K$$

Lean4

theorem relIndex_pointwise_smul [Group G] [MulDistribMulAction H G] (J K : Subgroup G) :
    (h • J).relIndex (h • K) = J.relIndex K := by
  rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def, comap_map_eq_self_of_injective (by intro a b; simp)]

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