Commit 2024-09-04 08:40 8ffca2e3

View on Github →

chore: remove a superfluous by in GroupTheory.Perm.Cycle.Factors (#16465)

Estimated changes

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

modified def Equiv.Perm.cycleFactorsAux