Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 22:19 5696275a

View on Github →

feat(data/list/big_operators): add list.sublist.prod_le_prod' etc (#13879)

  • add list.forall₂.prod_le_prod', list.sublist.prod_le_prod', and list.sublist_forall₂.prod_le_prod';
  • add their additive versions;
  • upgrade list.forall₂_same to an iff.

Estimated changes

modified theorem list.forall₂_eq_eq_eq
modified theorem list.forall₂_same