Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-09 06:19 fc6f57af

View on Github →

feat(data/list/basic): list.forall2, list.sections

Estimated changes

Modified data/list/basic.lean

added inductive list.forall₂

added theorem list.forall₂_cons

added theorem list.forall₂_iff_zip

added theorem list.forall₂_length_eq

added theorem list.forall₂_nil_left

added theorem list.forall₂_nil_right

added theorem list.forall₂_zip

added theorem list.mem_sections

added theorem list.mem_sections_length

added def list.sections