coset_relationtheoremProved here from basic factspropext
coset_relationLean 4Proved here from basic factsFormally verified
/-- "Lie in the same left coset of `H`" is an equivalence relation: `a ~ b ↔ a⁻¹ * b ∈ H`.Reflexive because `a⁻¹ * a = 1 ∈ H`; symmetric because `(a⁻¹ * b)⁻¹ = b⁻¹ * a`; transitivebecause `(a⁻¹ * b) * (b⁻¹ * c) = a⁻¹ * c`. Its classes are the left cosets `aH`. -/theorem coset_relation {G : Type*} [Group G] (H : Subgroup G) : Equivalence (fun a b : G => a⁻¹ * b ∈ H) where refl a := by simp symm {a b} h := by simpa [mul_inv_rev] using H.inv_mem h trans {a b c} h₁ h₂ := by simpa [mul_assoc] using H.mul_mem h₁ h₂
card_cosettheoremProved here from basic factspropext, Classical.choice, Quot.sound
card_cosetLean 4Proved here from basic factsFormally verified
/-- Every left coset `gH` has exactly as many elements as `H`: the map `h ↦ g * h` from `H`onto `gH` is injective, because `g * h = g * h'` forces `h = h'` (cancel `g`). -/theorem card_coset {G : Type*} [Group G] (H : Subgroup G) (g : G) : Nat.card ↥(g • (H : Set G)) = Nat.card H := by rw [← Set.image_smul] exact Nat.card_image_of_injective (fun a b h => mul_left_cancel h) _
lagrangetheoremApplies a library theorempropext, Classical.choice, Quot.sound
lagrangeLean 4Applies a library theoremFormally verified
/-- **Lagrange's theorem**: the order of a subgroup divides the order of the group.This applies Mathlib's `Subgroup.card_subgroup_dvd_card`, whose proof is the lesson's: thecosets partition `G` (`coset_relation`) into pieces of size `|H|` (`card_coset`). -/theorem lagrange {G : Type*} [Group G] (H : Subgroup G) : Nat.card H ∣ Nat.card G := Subgroup.card_subgroup_dvd_card H
card_mul_indextheoremApplies a library theorempropext, Classical.choice, Quot.sound
card_mul_indexLean 4Applies a library theoremFormally verified
/-- The precise form of Lagrange's theorem: `|G| = |H| · [G : H]`, where the index `[G : H]` isthe number of left cosets. This is Mathlib's `Subgroup.card_mul_index`. -/theorem card_mul_index {G : Type*} [Group G] (H : Subgroup G) : Nat.card H * H.index = Nat.card G := Subgroup.card_mul_index H
orderOf_dvdtheoremApplies a library theorempropext, Classical.choice, Quot.sound
orderOf_dvdLean 4Applies a library theoremFormally verified
/-- The order of an element divides the order of the group: apply Lagrange to the cyclicsubgroup `⟨g⟩`, which has `ord(g)` elements. This is Mathlib's `orderOf_dvd_natCard`. -/theorem orderOf_dvd {G : Type*} [Group G] (g : G) : orderOf g ∣ Nat.card G := orderOf_dvd_natCard g
pow_card_eq_onetheoremProved here from basic factspropext, Classical.choice, Quot.sound
pow_card_eq_oneLean 4Proved here from basic factsFormally verified
/-- For every element of a group, `g ^ |G| = 1`. Write `|G| = ord(g) · k` (by `orderOf_dvd`);then `g ^ |G| = (g ^ ord(g)) ^ k = 1 ^ k = 1`. For the group `(ℤ/pℤ)ˣ` of order `p - 1` this isFermat's little theorem. -/theorem pow_card_eq_one {G : Type*} [Group G] (g : G) : g ^ Nat.card G = 1 := by obtain ⟨k, hk⟩ := orderOf_dvd g rw [hk, pow_mul, pow_orderOf_eq_one, one_pow]
prime_order_cyclictheoremApplies a library theorempropext, Classical.choice, Quot.sound
prime_order_cyclicLean 4Applies a library theoremFormally verified
/-- A group of prime order `p` is cyclic: any element `g ≠ 1` has order dividing `p` anddifferent from `1`, so `⟨g⟩` is everything. This is Mathlib's `isCyclic_of_prime_card`. -/theorem prime_order_cyclic {G : Type*} [Group G] {p : ℕ} [Fact p.Prime] (h : Nat.card G = p) : IsCyclic G := isCyclic_of_prime_card h
subgroup_cyclictheoremApplies a library theorempropext, Classical.choice, Quot.sound
subgroup_cyclicLean 4Applies a library theoremFormally verified
/-- Every subgroup of a cyclic group is cyclic (generated by the smallest positive power of thegenerator that it contains). Mathlib provides this as the instance `Subgroup.isCyclic`. -/theorem subgroup_cyclic {G : Type*} [Group G] [IsCyclic G] (H : Subgroup G) : IsCyclic H := inferInstance
comm_of_sq_eq_onetheoremProved here from basic factspropext
comm_of_sq_eq_oneLean 4Proved here from basic factsFormally verified
/-- If every element squares to `1`, the group is abelian. Since `x * x = 1` means `x⁻¹ = x`:`a * b = (a * b)⁻¹ = b⁻¹ * a⁻¹ = b * a`. Example: the Klein four-group `ℤ/2 × ℤ/2`. -/theorem comm_of_sq_eq_one {G : Type*} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) : a * b = b * a := by have inv_self : ∀ x : G, x⁻¹ = x := fun x => inv_eq_of_mul_eq_one_right (h x) calc a * b = (a * b)⁻¹ := (inv_self (a * b)).symm _ = b⁻¹ * a⁻¹ := mul_inv_rev a b _ = b * a := by rw [inv_self a, inv_self b]
dihedral_not_commtheoremProved here from basic factspropext, Quot.sound
dihedral_not_commLean 4Proved here from basic factsFormally verified
/-- The symmetry group `D₃` of an equilateral triangle is not abelian: the rotation `r` by 120°and the reflection `s` satisfy `r * s ≠ s * r`. Mathlib's `DihedralGroup 3` has elements `r i`(rotations) and `sr i` (reflections); `decide` checks the multiplication table. -/theorem dihedral_not_comm : (DihedralGroup.r 1 : DihedralGroup 3) * DihedralGroup.sr 0 ≠ DihedralGroup.sr 0 * DihedralGroup.r 1 := by decide
sq_mem_of_index_twotheoremProved here from basic factspropext, Classical.choice, Quot.sound
sq_mem_of_index_twoLean 4Proved here from basic factsFormally verified
/-- A subgroup of index 2 contains every square. Mathlib's `Subgroup.index_eq_two_iff` gives an`a` such that, for every `b`, exactly one of `b * a` and `b` lies in `H`. If `g ∉ H` then`g * a ∈ H`; if also `g² ∉ H` then `g² * a ∈ H`, and so `g = (g² * a) * (g * a)⁻¹ ∈ H`,a contradiction. (Mathlib also has this as `Subgroup.sq_mem_of_index_two`.) -/theorem sq_mem_of_index_two {G : Type*} [Group G] {H : Subgroup G} (h : H.index = 2) (g : G) : g ^ 2 ∈ H := by obtain ⟨a, ha⟩ := Subgroup.index_eq_two_iff.mp h by_contra hsq have hg : g ∉ H := fun hg => hsq (by rw [pow_two]; exact H.mul_mem hg hg) have hga : g * a ∈ H := ((ha g).or).resolve_right hg have hgga : g ^ 2 * a ∈ H := ((ha (g ^ 2)).or).resolve_right hsq apply hg have key : g = (g ^ 2 * a) * (g * a)⁻¹ := by group rw [key] exact H.mul_mem hgga (H.inv_mem hga)
card_alternating_fourtheoremProved here from basic factspropext, Classical.choice, Quot.sound
card_alternating_fourLean 4Proved here from basic factsFormally verified
/-- The alternating group `A₄` of even permutations of four objects has `4!/2 = 12` elements.Mathlib's `nat_card_alternatingGroup` gives `|Aₙ| = n!/2`; the rest is arithmetic. -/theorem card_alternating_four : Nat.card (alternatingGroup (Fin 4)) = 12 := by rw [nat_card_alternatingGroup] simp [Nat.card_eq_fintype_card, Fintype.card_fin] decide
squares_alternating_fourtheoremProved here from basic factspropext, Classical.choice, Quot.sound
squares_alternating_fourLean 4Proved here from basic factsFormally verified
/-- In `A₄` exactly nine elements are squares: the identity and the eight 3-cycles (each 3-cycle`c` is the square of `c²`), while the squares of the three double transpositions are `1`.Checked by `decide` over all twelve elements. -/theorem squares_alternating_four : (Finset.univ.image (fun g : alternatingGroup (Fin 4) => g ^ 2)).card = 9 := by decide
alternating_four_no_subgroup_of_order_sixtheoremProved here from basic factspropext, Classical.choice, Quot.sound
alternating_four_no_subgroup_of_order_sixLean 4Proved here from basic factsFormally verified
/-- **The converse of Lagrange's theorem fails**: `A₄` has order 12, and 6 divides 12, but `A₄`has no subgroup of order 6. Such a subgroup would have index 2 (`|G| = |H| · [G : H]`), so itwould contain all nine squares (`sq_mem_of_index_two`, `squares_alternating_four`) — too manyfor a set of six elements. -/theorem alternating_four_no_subgroup_of_order_six : ¬ ∃ H : Subgroup (alternatingGroup (Fin 4)), Nat.card H = 6 := by rintro ⟨H, hH⟩ have hindex : H.index = 2 := by have h := Subgroup.card_mul_index H rw [hH, card_alternating_four] at h omega -- All nine squares lie in `H`, viewed as a finite set. classical have hsub : Finset.univ.image (fun g : alternatingGroup (Fin 4) => g ^ 2) ⊆ Finset.univ.filter (· ∈ H) := by intro x hx obtain ⟨g, -, rfl⟩ := Finset.mem_image.mp hx simpa using sq_mem_of_index_two hindex g have hcard := Finset.card_le_card hsub rw [squares_alternating_four, ← Fintype.card_subtype, ← Nat.card_eq_fintype_card] at hcard have h6 : Nat.card {x // x ∈ H} = 6 := hH omega
ker_normaltheoremProved here from basic factspropext
ker_normalLean 4Proved here from basic factsFormally verified
/-- The kernel of a homomorphism is a normal subgroup: if `f n = 1` then`f (g * n * g⁻¹) = f g * 1 * (f g)⁻¹ = 1`. (Mathlib records this as the instance`MonoidHom.normal_ker`.) -/theorem ker_normal {G H : Type*} [Group G] [Group H] (f : G →* H) : f.ker.Normal where conj_mem n hn g := by rw [MonoidHom.mem_ker] at hn ⊢ rw [map_mul, map_mul, hn, mul_one, map_inv, mul_inv_cancel]
ker_coset_actiontheoremProved here from basic factspropext, Classical.choice, Quot.sound
ker_coset_actionLean 4Proved here from basic factsFormally verified
/-- **Every normal subgroup is a kernel.** `G` acts on the set `G ⧸ N` of left cosets by`g · aN = (g * a)N`, giving a homomorphism `G → Perm (G ⧸ N)`. Its kernel is exactly `N`:`g` fixes every coset `aN` iff `a⁻¹ * g * a ∈ N` for all `a`, which for normal `N` says `g ∈ N`.No quotient *group* is needed — only the set of cosets. -/theorem ker_coset_action {G : Type*} [Group G] (N : Subgroup G) [hN : N.Normal] : (MulAction.toPermHom G (G ⧸ N)).ker = N := by ext g rw [MonoidHom.mem_ker] constructor · intro h -- `g` fixes the coset `1 · N`, so `gN = N`. have h1 : g • (QuotientGroup.mk 1 : G ⧸ N) = QuotientGroup.mk 1 := by have := congrArg (fun σ : Perm (G ⧸ N) => σ (QuotientGroup.mk 1)) h simpa using this rw [MulAction.Quotient.smul_mk, QuotientGroup.eq] at h1 simpa using h1 · intro hg ext x induction x using QuotientGroup.induction_on with | H a => show g • (QuotientGroup.mk a : G ⧸ N) = QuotientGroup.mk a rw [MulAction.Quotient.smul_mk, QuotientGroup.eq] -- `(g * a)⁻¹ * a = a⁻¹ * g⁻¹ * a`, a conjugate of `g⁻¹ ∈ N`. have := hN.conj_mem g⁻¹ (N.inv_mem hg) a⁻¹ simpa [mul_assoc] using this
orbit_stabilizertheoremApplies a library theorempropext, Classical.choice, Quot.sound
orbit_stabilizerLean 4Applies a library theoremFormally verified
/-- **Orbit–stabiliser**: for a finite group acting on `X`, `|G · x| · |Gₓ| = |G|`.This applies Mathlib's `MulAction.card_orbit_mul_card_stabilizer_eq_card_group`, proved (as inthe lesson) from the bijection `G ⧸ Gₓ ≃ G · x`, `gGₓ ↦ g · x`. -/theorem orbit_stabilizer {G X : Type*} [Group G] [MulAction G X] [Fintype G] (x : X) [Fintype (MulAction.orbit G x)] [Fintype (MulAction.stabilizer G x)] : Fintype.card (MulAction.orbit G x) * Fintype.card (MulAction.stabilizer G x) = Fintype.card G := MulAction.card_orbit_mul_card_stabilizer_eq_card_group G x
burnsidetheoremApplies a library theorempropext, Classical.choice, Quot.sound
burnsideLean 4Applies a library theoremFormally verified
/-- **Burnside's lemma** (Cauchy–Frobenius): the number of orbits times `|G|` is the total numberof fixed points, `Σ_g |Fix(g)|`. This is Mathlib's`MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group`; here `Ω` is the set of orbits. -/theorem burnside {G X : Type*} [Group G] [MulAction G X] [Fintype G] [∀ g : G, Fintype (MulAction.fixedBy X g)] [Fintype (MulAction.orbitRel.Quotient G X)] : ∑ g : G, Fintype.card (MulAction.fixedBy X g) = Fintype.card (MulAction.orbitRel.Quotient G X) * Fintype.card G := MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group G X
cayleytheoremProved here from basic factspropext, Classical.choice, Quot.sound
cayleyLean 4Proved here from basic factsFormally verified
/-- **Cayley's theorem**: every group is isomorphic to a group of permutations. The leftregular action `g · x = g * x` gives a homomorphism `G → Perm G`, and it is injective: if `g`and `h` act alike, then `g = g * 1 = h * 1 = h`. -/theorem cayley {G : Type*} [Group G] : Function.Injective (MulAction.toPermHom G G) := by intro g h hgh have := congrArg (fun σ : Perm G => σ 1) hgh simpa using this
/-- If every element of a group squares to `1`, the group is abelian.Hint: first show `x⁻¹ = x` for every `x` (`inv_eq_of_mul_eq_one_right`), then compute`a * b = (a * b)⁻¹ = b⁻¹ * a⁻¹` (`mul_inv_rev`). -/theorem comm_of_sq_eq_one {G : Type*} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) : a * b = b * a := by sorry
Show the compiled solution
comm_of_sq_eq_oneLean 4Proved here from basic factsFormally verified
/-- If every element squares to `1`, the group is abelian. Since `x * x = 1` means `x⁻¹ = x`:`a * b = (a * b)⁻¹ = b⁻¹ * a⁻¹ = b * a`. Example: the Klein four-group `ℤ/2 × ℤ/2`. -/theorem comm_of_sq_eq_one {G : Type*} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) : a * b = b * a := by have inv_self : ∀ x : G, x⁻¹ = x := fun x => inv_eq_of_mul_eq_one_right (h x) calc a * b = (a * b)⁻¹ := (inv_self (a * b)).symm _ = b⁻¹ * a⁻¹ := mul_inv_rev a b _ = b * a := by rw [inv_self a, inv_self b]
/-- Every element satisfies `g ^ |G| = 1`.Hint: `orderOf_dvd_natCard g` gives `k` with `Nat.card G = orderOf g * k`; then use `pow_mul`and `pow_orderOf_eq_one`. -/theorem pow_card_eq_one {G : Type*} [Group G] (g : G) : g ^ Nat.card G = 1 := by sorry
Show the compiled solution
pow_card_eq_oneLean 4Proved here from basic factsFormally verified
/-- For every element of a group, `g ^ |G| = 1`. Write `|G| = ord(g) · k` (by `orderOf_dvd`);then `g ^ |G| = (g ^ ord(g)) ^ k = 1 ^ k = 1`. For the group `(ℤ/pℤ)ˣ` of order `p - 1` this isFermat's little theorem. -/theorem pow_card_eq_one {G : Type*} [Group G] (g : G) : g ^ Nat.card G = 1 := by obtain ⟨k, hk⟩ := orderOf_dvd g rw [hk, pow_mul, pow_orderOf_eq_one, one_pow]
/-- Cayley's theorem: the left regular action `G → Perm G` is injective.Hint: apply both permutations to `1`. -/theorem cayley {G : Type*} [Group G] : Function.Injective (MulAction.toPermHom G G) := by sorry
Show the compiled solution
cayleyLean 4Proved here from basic factsFormally verified
/-- **Cayley's theorem**: every group is isomorphic to a group of permutations. The leftregular action `g · x = g * x` gives a homomorphism `G → Perm G`, and it is injective: if `g`and `h` act alike, then `g = g * 1 = h * 1 = h`. -/theorem cayley {G : Type*} [Group G] : Function.Injective (MulAction.toPermHom G G) := by intro g h hgh have := congrArg (fun σ : Perm G => σ 1) hgh simpa using this