permutations

Stream: new members

[vxctyxeha]

Do these two sides represent different sets?

({σ : Perm (Fin 4) | σ.cycleType = {4}} : Finset (Perm (Fin 4))) = ((univ : Finset (Perm (Fin 4))).filter (fun σ => σ.cycleType = {4}) : Finset (Perm (Fin 4)))

[Aaron Liu]

no, they are "syntactically" equal

[vxctyxeha]

"Is the code below equivalent to proving what all the 4-cycles in S4 are?

import Mathlib
open Equiv Equiv.Perm Finset

theorem S4 :  ({ c[0,1,2,3], c[0,1,3,2], c[0,2,1,3], c[0,2,3,1], c[0,3,2,1], c[0,3,1,2] } : Finset (Perm (Fin 4))) = ((univ : Finset (Perm (Fin 4))).filter (fun σ => σ.cycleType = {4}) : Finset (Perm (Fin 4))) --
    := by

      native_decide

[vxctyxeha]

import Mathlib

open Equiv Equiv.Perm Finset

theorem per :

  ({ 1,  c[0, 1, 2], (c[0, 1, 2])^2, c[0, 1], c[0, 1, 2] * c[0, 1], ((c[0, 1, 2])^2) * c[0, 1] } : Finset (Perm (Fin 3))) = (univ : Finset (Perm (Fin 3))) :=

by
-

  decide