Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-02 10:49 d6789b8b

View on Github →

refactor(data/list/forall2): consistent names of relations (#16098)

Estimated changes

Modified src/data/list/forall2.lean

modified theorem list.forall₂.flip

modified theorem list.forall₂.imp

modified theorem list.forall₂.length_eq

modified theorem list.forall₂.mp

modified theorem list.forall₂_and_left

modified theorem list.forall₂_cons

modified theorem list.forall₂_drop

modified theorem list.forall₂_drop_append

modified theorem list.forall₂_iff_zip

modified theorem list.forall₂_nil_left_iff

modified theorem list.forall₂_nil_right_iff

modified theorem list.forall₂_refl

modified theorem list.forall₂_reverse_iff

modified theorem list.forall₂_same

modified theorem list.forall₂_take

modified theorem list.forall₂_take_append

modified theorem list.forall₂_zip

modified theorem list.left_unique_forall₂'

modified theorem list.rel_append

modified theorem list.rel_bind

modified theorem list.rel_filter_map

modified theorem list.rel_foldl

modified theorem list.rel_foldr

modified theorem list.rel_join

modified theorem list.rel_map

modified theorem list.rel_mem

modified theorem list.rel_reverse

modified theorem list.right_unique_forall₂'

modified theorem list.sublist.sublist_forall₂

modified inductive list.sublist_forall₂

modified theorem list.tail_sublist_forall₂_self

modified theorem relator.bi_unique.forall₂

modified theorem relator.left_unique.forall₂

modified theorem relator.right_unique.forall₂