map

Stream: mathlib4

[vxctyxeha]

how to define a map from s3 to z2

import Mathlib


open Equiv Equiv.Perm
open Equiv Equiv.Perm Additive
def toFun₀ : Perm (Fin 3) → ZMod 4
  | 1 => 0
  | c[0, 1] => 1
  | c[0, 2] => 2
  | c[1, 2]  => 3
  | c[0, 1, 2]=> 0
  | c[0, 2, 1] => 1

[Yury G. Kudryashov]

Please provide more details:

• why do you want to do this?
• why this particular map is interesting?
• what have you tried and how it fails?