theorem Lagrange.card_eq_index_mul_card {G : Type u_1} [Group G] [Fintype G] (H : Subgroup G) [Fintype ↥H] : Fintype.card G = H.index * Fintype.card ↥H

theorem Lagrange.lagrange_dvd (G : Type u_1) [Group G] [Fintype G] (H : Subgroup G) [Fintype ↥H] : Fintype.card ↥H ∣ Fintype.card G

theorem Lagrange.lagrange_theorem (G : Type u_1) [Group G] [Fintype G] (H : Subgroup G) [Fintype ↥H] : Fintype.card ↥H ∣ Fintype.card G

theorem Lagrange.counting_formula {G : Type u_1} [Group G] [Fintype G] (H : Subgroup G) [Fintype ↥H] : Fintype.card G = Fintype.card ↥H * H.index