Commit 2023-11-23 03:28 6834a65f

View on Github →

feat: add List.enum_eq_nil and List.mapIdx_eq_nil (#8493) Adds List.enum_eq_nil and List.mapIdx_eq_nil. These are analogous to List.map_eq_nil.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.enumFrom_eq_nil

added theorem List.enum_eq_nil

Modified Mathlib/Data/List/Indexes.lean

added theorem List.mapIdx_eq_nil