Commit 2024-05-06 10:56 5bd44fb3

View on Github →

chore(Data/List/Forall): more migration nthLe -> get (#12645) Rewrite List.Forall₂.nthLe and some related theorems in terms of get.

Estimated changes

Modified Mathlib/Data/List/Forall2.lean

added theorem List.Forall₂.get

modified theorem List.Forall₂.nthLe

added theorem List.forall₂_iff_get

modified theorem List.forall₂_iff_nthLe

added theorem List.forall₂_of_length_eq_of_get

modified theorem List.forall₂_of_length_eq_of_nthLe