Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 07:10 bb289539

View on Github →

feat(data/list/forall2): add list.forall₂_iff_nth_le (#16073) Characterization of list.forall₂ with respect to list.nth_le on all positions.

Estimated changes

Modified src/data/list/forall2.lean

added theorem list.forall₂.length_eq

added theorem list.forall₂.nth_le

added theorem list.forall₂_iff_nth_le

deleted theorem list.forall₂_length_eq

added theorem list.forall₂_of_length_eq_of_nth_le

Modified src/data/list/sections.lean