conj_class

Stream: new members

[vxctyxeha]

hello i want to list all the conj class of S4，My plan is to use a representative element to see if there is a simpler method.

import Mathlib
open Equiv.Perm ConjClasses Finset Set



example : ConjClasses.carrier (ConjClasses.mk (1 )) =
          ({ (1 ) } : Set (Equiv.Perm (Fin 3))) := by
  ext g
  simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj, isConj_one_right, Set.mem_singleton_iff]
  exact isConj_one_left

example : ConjClasses.carrier (ConjClasses.mk (Equiv.swap (0 : Fin 3) 1)) =
          ( { Equiv.swap (0 : Fin 3) 1, Equiv.swap (0 : Fin 3) 2, Equiv.swap (1 : Fin 3) 2 } : Set (Equiv.Perm (Fin 3))) := by
  sorry

[Notification Bot]

This topic was moved here from #new members > light test by vxctyxeha.