Index_of_Intersection_of_Subgroups
Provedgroup-theoryindexproofwikisubgroup
Let G be a group and H, K subgroups of finite index. Then [G : H ∩ K] ≤ [G : H] * [G : K].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Index_of_Intersection_of_Subgroups {G : Type _} [Group G] (H K : Subgroup G) (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≤ H.index * K.index := by sorrySource