Commit 2024-02-27 06:49 2414ba09

View on Github →

chore(GroupTheory/Perm): drop DecidableEq, Fintype -> Finite (#10917)

Estimated changes

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

modified theorem Equiv.Perm.Disjoint.isConj_mul

modified def Equiv.Perm.cycleFactorsAux

modified theorem Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff

modified theorem Equiv.Perm.fixed_point_card_lt_of_ne_one

modified def Equiv.Perm.truncCycleFactors

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified theorem Equiv.Perm.signAux3_symm_trans_trans