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

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

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

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

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

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

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

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

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

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_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_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} (hHK : H ≤ K) : Nat.card { x : α // x ∈ H } ∣ Nat.card { x : α // x ∈ K }

theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} (hHK : H ≤ K) : Nat.card { x : α // x ∈ H } ∣ Nat.card { x : α // x ∈ 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 { x : α // x ∈ AddSubgroup.comap f K } ∣ Nat.card { x : H // x ∈ 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 { x : α // x ∈ Subgroup.comap f K } ∣ Nat.card { x : H // x ∈ K }