conjcalss

Stream: new members

[vxctyxeha]

hello i try to prove that There does not exist a group of order 15 whose class equation is $15 = 1 + 2 + 2 + 2 + 2 + 2 + 2 + 2$. But I don't know how to express it precisely.and i know Conjugacy classes form a partition of G, The code shown below is what I have tried.

import Mathlib

open scoped Classical
open Subgroup

/-- The size of a conjugacy class divides the order of the group. -/
lemma card_conj_class_dvd_card_group {G : Type*} [Group G] [Fintype G] (g : G) :
    Fintype.card (ConjClasses.mk g).carrier ∣ Fintype.card G := by
  -- By the orbit-stabilizer theorem
  have h := ConjClasses.card_carrier g
  let H := MulAction.stabilizer (ConjAct G) g
  have hdvd : Fintype.card H ∣ Fintype.card G := by
    have := @Subgroup.card_subgroup_dvd_card G _ H
    simp only [Nat.card_eq_fintype_card] at this
    exact this
  rw [h]
  exact Nat.div_dvd_of_dvd hdvd

/-- A group of order 15 cannot have a conjugacy class of size 2. -/
lemma no_conj_class_of_size_two_in_group_of_order_15
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 15) :
    ∀ g : G, Fintype.card (ConjClasses.mk g).carrier ≠ 2 := by
  intro g h_card_2
  have h_dvd := card_conj_class_dvd_card_group g
  rw [h_card_2, hG] at h_dvd
  norm_num at h_dvd