Metamath Proof Explorer
Table of Contents - 10.2.10.5. The sign of a permutation
- cpsgn
- cevpm
- df-psgn
- df-evpm
- psgnunilem1
- psgnunilem5
- psgnunilem2
- psgnunilem3
- psgnunilem4
- m1expaddsub
- psgnuni
- psgnfval
- psgnfn
- psgndmsubg
- psgneldm
- psgneldm2
- psgneldm2i
- psgneu
- psgnval
- psgnvali
- psgnvalii
- psgnpmtr
- psgn0fv0
- sygbasnfpfi
- psgnfvalfi
- psgnvalfi
- psgnran
- gsmtrcl
- psgnfitr
- psgnfieu
- pmtrsn
- psgnsn
- psgnprfval
- psgnprfval1
- psgnprfval2