Commit 2024-04-17 13:43 6d66f4ca

View on Github →

chore(Data/List/Enum): move from Basic (#11697)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.enumFrom_append

deleted theorem List.enumFrom_cons'

deleted theorem List.enumFrom_eq_nil

deleted theorem List.enumFrom_get?

deleted theorem List.enumFrom_map

deleted theorem List.enumFrom_map_snd

deleted theorem List.enumFrom_singleton

deleted theorem List.enum_append

deleted theorem List.enum_cons'

deleted theorem List.enum_cons

deleted theorem List.enum_eq_nil

deleted theorem List.enum_get?

deleted theorem List.enum_map

deleted theorem List.enum_map_snd

deleted theorem List.enum_nil

deleted theorem List.enum_singleton

deleted theorem List.get_enum

deleted theorem List.get_enumFrom

deleted theorem List.map_fst_add_enumFrom_eq_enumFrom

deleted theorem List.map_fst_add_enum_eq_enumFrom

deleted theorem List.mem_enumFrom

deleted theorem List.nthLe_enum

deleted theorem List.nthLe_enumFrom

Created Mathlib/Data/List/Enum.lean

added theorem List.enumFrom_append

added theorem List.enumFrom_cons'

added theorem List.enumFrom_eq_nil

added theorem List.enumFrom_get?

added theorem List.enumFrom_map

added theorem List.enumFrom_map_snd

added theorem List.enumFrom_singleton

added theorem List.enum_append

added theorem List.enum_cons'

added theorem List.enum_cons

added theorem List.enum_eq_nil

added theorem List.enum_get?

added theorem List.enum_map

added theorem List.enum_map_snd

added theorem List.enum_nil

added theorem List.enum_singleton

added theorem List.get_enum

added theorem List.get_enumFrom

added theorem List.map_fst_add_enumFrom_eq_enumFrom

added theorem List.map_fst_add_enum_eq_enumFrom

added theorem List.mem_enumFrom

added theorem List.nthLe_enum

added theorem List.nthLe_enumFrom

Modified Mathlib/Data/List/Range.lean