Commit 2025-12-06 12:38 64aed99c

View on Github →

feat(Data/List/Basic): idxOf lemmas (#31930)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.IsPrefix.idxOf_eq_of_mem

added theorem List.IsPrefix.idxOf_le

added theorem List.IsSuffix.idxOf_add_length_le

added theorem List.IsSuffix.idxOf_le

added theorem List.idxOf_eq_zero_iff_eq_nil_or_head_eq

added theorem List.idxOf_eq_zero_iff_head_eq