Lagrange's theorem: the order of a subgroup divides the order of the group.

theorem Subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

theorem AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

theorem Subgroup.card_mul_eq_card_subgroup_mul_card_quotient {α : Type u_1} [Group α] (s : Subgroup α) (t : Set α) : Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

theorem AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotient {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set α) : Nat.card ↑(t + ↑s) = Nat.card ↥s * Nat.card ↑(QuotientAddGroup.mk '' t)

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card ↥s ∣ Nat.card α

Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.

theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card ↥s ∣ Nat.card α

Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.

theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

theorem AddSubgroup.card_quotient_dvd_card {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

theorem Subgroup.card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (hf : Function.Injective ⇑f) : Nat.card α ∣ Nat.card H

theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (hf : Function.Injective ⇑f) : Nat.card α ∣ Nat.card H

theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem Subgroup.card_comap_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (K : Subgroup H) (f : α →* H) (hf : Function.Injective ⇑f) : Nat.card ↥(Subgroup.comap f K) ∣ Nat.card ↥K

theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (K : AddSubgroup H) (f : α →+ H) (hf : Function.Injective ⇑f) : Nat.card ↥(AddSubgroup.comap f K) ∣ Nat.card ↥K