Commit 2024-02-14 20:20 b2c40e86

View on Github →

chore(Perm/Sign): Fintype -> Finite (#10549)

Estimated changes

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified def Equiv.Perm.signAux3

modified theorem Equiv.Perm.signAux3_mul_and_swap

modified theorem Equiv.Perm.subtypePermOfFintype_apply

modified theorem Equiv.Perm.subtypePermOfFintype_one