Documentation

Mathlib.GroupTheory.Coset.Card

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

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 α) :

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

theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [Group α] (s : Subgroup α) :
theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (f : α →+ H) (hf : Function.Injective f) :
theorem Subgroup.card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (hf : Function.Injective f) :
theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} (hHK : H K) :
theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} (hHK : H 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) :
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) :