Commit 2023-07-18 07:35 593a84d5

View on Github →

chore: forward port #18999 (#5974)

Estimated changes

Modified Mathlib/Data/Fin/Tuple/BubbleSortInduction.lean

Modified Mathlib/Data/Fintype/Card.lean

deleted theorem Finite.Preorder.wellFounded_gt

deleted theorem Finite.Preorder.wellFounded_lt