Lagrange's theorem: the order of a subgroup divides the order of the group. #
Subgroup.card_subgroup_dvd_card
: Lagrange's theorem (for multiplicative groups); there is an analogous version for additive groups
instance
QuotientGroup.fintype
{α : Type u_1}
[Group α]
[Fintype α]
(s : Subgroup α)
[DecidableRel ⇑(leftRel s)]
:
Equations
instance
QuotientAddGroup.fintype
{α : Type u_1}
[AddGroup α]
[Fintype α]
(s : AddSubgroup α)
[DecidableRel ⇑(leftRel s)]
:
Equations
instance
QuotientAddGroup.fintypeQuotientRightRel
{α : Type u_1}
[AddGroup α]
{s : AddSubgroup α}
[Fintype (α ⧸ s)]
:
theorem
QuotientAddGroup.card_quotient_rightRel
{α : Type u_1}
[AddGroup α]
(s : AddSubgroup α)
[Fintype (α ⧸ s)]
:
theorem
AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotient
{α : Type u_1}
[AddGroup α]
(s : AddSubgroup α)
(t : Set α)
:
Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.
theorem
AddSubgroup.card_dvd_of_le
{α : Type u_1}
[AddGroup α]
{H K : AddSubgroup α}
(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)
: