Commit 2023-09-15 18:54 d7030312

View on Github →

feat(Data/List/Range + Data/Finset/Sort): List.finRange lemmas (#7184) Prove Fin.sort_univ and List.indexOf_finRange discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20value.20of.20.60fintypeEquivFin.60

Estimated changes

Modified Mathlib/Data/Finset/Sort.lean

added theorem Fin.sort_univ

Modified Mathlib/Data/Fintype/Basic.lean

added theorem List.toFinset_finRange

Modified Mathlib/Data/List/Range.lean

added theorem List.indexOf_finRange

added theorem List.pairwise_le_finRange

added theorem List.pairwise_lt_finRange