Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-26 00:55 fd1c8e7f

View on Github →

feat(data/list/forall2): add two lemmas about forall₂ and reverse (#7714) rel_reverse shows that forall₂ is preserved across reversed lists, forall₂_iff_reverse uses rel_reverse to show that it is preserved in both directions.

Estimated changes