Mathlib.GroupTheory.Coset.Card

Subgroup.card_eq_card_quotient_mul_card_subgroup theorem

(s : Subgroup α) : Nat.card α = Nat.card (α ⧸ s) * Nat.card s

Full source

@[to_additive AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup]
theorem card_eq_card_quotient_mul_card_subgroup (s : Subgroup α) :
    Nat.card α = Nat.card (α ⧸ s) * Nat.card s := by
  rw [← Nat.card_prod]; exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

Lagrange's Theorem: Group Order Equals Quotient Order Times Subgroup Order

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, the cardinality of $\alpha$ is equal to the product of the cardinality of the quotient group $\alpha ⧸ s$ and the cardinality of $s$, i.e., $|\alpha| = |\alpha ⧸ s| \cdot |s|$.

Subgroup.card_mul_eq_card_subgroup_mul_card_quotient theorem

(s : Subgroup α) (t : Set α) : Nat.card (t * s : Set α) = Nat.card s * Nat.card (t.image (↑) : Set (α ⧸ s))

Full source

@[to_additive]
lemma card_mul_eq_card_subgroup_mul_card_quotient (s : Subgroup α) (t : Set α) :
    Nat.card (t * s : Set α) = Nat.card s * Nat.card (t.image (↑) : Set (α ⧸ s)) := by
  rw [← Nat.card_prod, Nat.card_congr]
  apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)
  rw [QuotientGroup.preimage_image_mk]
  convert Equiv.refl ↑(t * s)
  aesop (add simp [Set.mem_mul])

Cardinality of Product Set Equals Product of Subgroup and Quotient Cardinalities

Informal description

Let $G$ be a group with a subgroup $H$, and let $T$ be a subset of $G$. Then the cardinality of the product set $T \cdot H$ equals the product of the cardinality of $H$ and the cardinality of the image of $T$ in the quotient group $G/H$, i.e., \[ |T \cdot H| = |H| \cdot |\pi(T)| \] where $\pi: G \to G/H$ is the canonical projection map.

Subgroup.card_subgroup_dvd_card theorem

(s : Subgroup α) : Nat.card s ∣ Nat.card α

Full source

/-- **Lagrange's Theorem**: The order of a subgroup divides the order of its ambient group. -/
@[to_additive "**Lagrange's Theorem**: The order of an additive subgroup divides the order of its
 ambient additive group."]
theorem card_subgroup_dvd_card (s : Subgroup α) : Nat.cardNat.card s ∣ Nat.card α := by
  classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

Lagrange's Theorem: Subgroup Order Divides Group Order

Informal description

For any group $G$ and subgroup $H$ of $G$, the order of $H$ divides the order of $G$, i.e., $|H|$ divides $|G|$.

Subgroup.card_quotient_dvd_card theorem

(s : Subgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

Full source

@[to_additive]
theorem card_quotient_dvd_card (s : Subgroup α) : Nat.cardNat.card (α ⧸ s) ∣ Nat.card α := by
  simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]

Quotient Group Order Divides Group Order in Lagrange's Theorem

Informal description

For any group $\alpha$ and subgroup $s$ of $\alpha$, the cardinality of the quotient group $\alpha ⧸ s$ divides the cardinality of $\alpha$, i.e., $|\alpha ⧸ s|$ divides $|\alpha|$.

Subgroup.card_dvd_of_injective theorem

(f : α →* H) (hf : Function.Injective f) : Nat.card α ∣ Nat.card H

Full source

@[to_additive]
theorem card_dvd_of_injective (f : α →* H) (hf : Function.Injective f) :
    Nat.cardNat.card α ∣ Nat.card H := by
  classical calc
      Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
      _ ∣ Nat.card H := card_subgroup_dvd_card _

Lagrange's Theorem for Injective Group Homomorphisms: $|G|$ divides $|H|$

Informal description

For any group homomorphism $f \colon G \to H$ that is injective, the order of $G$ divides the order of $H$, i.e., $|G|$ divides $|H|$.

Subgroup.card_dvd_of_le theorem

{H K : Subgroup α} (hHK : H ≤ K) : Nat.card H ∣ Nat.card K

Full source

@[to_additive]
theorem card_dvd_of_le {H K : Subgroup α} (hHK : H ≤ K) : Nat.cardNat.card H ∣ Nat.card K :=
  card_dvd_of_injective (inclusion hHK) (inclusion_injective hHK)

Lagrange's Theorem for Subgroup Inclusion: $|H|$ divides $|K|$

Informal description

For any subgroups $H$ and $K$ of a group $\alpha$ such that $H \leq K$, the order of $H$ divides the order of $K$, i.e., $|H|$ divides $|K|$.

Subgroup.card_comap_dvd_of_injective theorem

(K : Subgroup H) (f : α →* H) (hf : Function.Injective f) : Nat.card (K.comap f) ∣ Nat.card K

Full source

@[to_additive]
theorem card_comap_dvd_of_injective (K : Subgroup H) (f : α →* H)
    (hf : Function.Injective f) : Nat.cardNat.card (K.comap f) ∣ Nat.card K :=
  calc Nat.card (K.comap f) = Nat.card ((K.comap f).map f) :=
      Nat.card_congr (equivMapOfInjective _ _ hf).toEquiv
    _ ∣ Nat.card K := card_dvd_of_le (map_comap_le _ _)

Lagrange's Theorem for Preimage Subgroups: $|K.\text{comap}\, f|$ divides $|K|$

Informal description

For any subgroup $K$ of a group $H$ and any injective group homomorphism $f \colon \alpha \to H$, the order of the preimage subgroup $K.\text{comap}\, f$ divides the order of $K$, i.e., $|K.\text{comap}\, f|$ divides $|K|$.