Commit 2022-10-10 08:47 11156f5a

View on Github →

feat(data/list/basic): Alias for length_le_of_sublist (#16841) Make an alias list.sublist.length_le of list.length_le_of_sublist and use it. Rename list.eq_of_sublist_of_length_eq and list.eq_of_sublist_of_length_le to use dot notation.

Estimated changes

Modified src/data/list/basic.lean

deleted theorem list.eq_of_sublist_of_length_eq

deleted theorem list.eq_of_sublist_of_length_le

modified theorem list.sublist.antisymm

added theorem list.sublist.eq_of_length

added theorem list.sublist.eq_of_length_le

Modified src/data/list/count.lean

Modified src/data/list/infix.lean

modified theorem list.is_infix.length_le

modified theorem list.is_prefix.length_le

modified theorem list.is_suffix.length_le

Modified src/data/list/perm.lean

Modified src/data/list/range.lean

Modified src/data/list/sublists.lean

Modified src/data/multiset/basic.lean

Modified src/group_theory/free_group.lean

modified theorem free_group.red.length_le

Modified src/number_theory/arithmetic_function.lean