Order_of_Subgroup_Product_v4
Provedgroup-theoryorderproofwikisubgroup
Let G be a group and H, K subgroups. Then |H| * |K| = |H ∩ K| * |HK|.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Subgroup_Product_v4 {G : Type _} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K] [Fintype ↑(H ⊓ K)] : Fintype.card H * Fintype.card K = Fintype.card ↑(H ⊓ K) * Nat.card {g : G | ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ g = h * k} := by sorrySource