Commit 2023-02-06 16:08 4d0921d2

View on Github →

feat: port Data.Fin.Tuple.BubbleSortInduction (#2107)

Estimated changes

Modified Mathlib.lean

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

added theorem Tuple.bubble_sort_induction'

added theorem Tuple.bubble_sort_induction