relIndex_pointwise_smul — Mathlib

English

Same invariance under pointwise smul for AddSubgroups: (h • J).relIndex (h • K) = J.relIndex K.

Русский

Та же инвариантность под действием по • для AddSubgroup: (h • J).relIndex (h • K) = J.relIndex K.

LaTeX

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

Lean4

theorem relIndex_pointwise_smul [AddGroup G] [DistribMulAction H G] (J K : AddSubgroup 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)]

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