Commit 2025-01-22 10:18 887629ed

View on Github →

chore: rename List.indexOf_lt_length to List.indexOf_lt_length_iff (#20939)

Estimated changes

Modified Mathlib/Data/FinEnum.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.indexOf_lt_length

added theorem List.indexOf_lt_length_iff

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

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

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified scripts/add_deprecations.sh