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)] : Fintype (α ⧸ s)

Equations

• QuotientGroup.fintype s = Quotient.fintype (QuotientGroup.leftRel s)

instance QuotientAddGroup.fintype {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [DecidableRel ⇑(leftRel s)] : Fintype (α ⧸ s)

Equations

• QuotientAddGroup.fintype s = Quotient.fintype (QuotientAddGroup.leftRel s)

@[instance 100]

instance QuotientGroup.finite {α : Type u_1} [Group α] {s : Subgroup α} [Finite α] : Finite (α ⧸ s)

@[instance 100]

instance QuotientAddGroup.finite {α : Type u_1} [AddGroup α] {s : AddSubgroup α} [Finite α] : Finite (α ⧸ s)

instance QuotientGroup.fintypeQuotientRightRel {α : Type u_1} [Group α] {s : Subgroup α} [Fintype (α ⧸ s)] : Fintype (Quotient (rightRel s))

Equations

• QuotientGroup.fintypeQuotientRightRel = Fintype.ofEquiv (α ⧸ s) (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

instance QuotientAddGroup.fintypeQuotientRightRel {α : Type u_1} [AddGroup α] {s : AddSubgroup α} [Fintype (α ⧸ s)] : Fintype (Quotient (rightRel s))

Equations

• QuotientAddGroup.fintypeQuotientRightRel = Fintype.ofEquiv (α ⧸ s) (QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s).symm

theorem QuotientGroup.card_quotient_rightRel {α : Type u_1} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (rightRel s)) = Fintype.card (α ⧸ s)

theorem QuotientAddGroup.card_quotient_rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (rightRel s)) = Fintype.card (α ⧸ s)

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 K : Subgroup α} (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H 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 ↥(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 ↥(comap f K) ∣ Nat.card ↥K