Tower_Law_for_Subgroups
Provedgroup-theoryindexproofwikisubgrouptower-law
Let G be a group, H a subgroup of G with finite index, and K a subgroup of H. Then [G : K] = [G : H] * [H : K].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Tower_Law_for_Subgroups {G : Type _} [Group G] (H K : Subgroup G) (hKH : K ≤ H) : K.index = H.index * (K.subgroupOf H).index := by sorrySource