Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 09:53 ff72aa22

View on Github →

feat(data/list/big_operators): add multiplicative versions (#12966)

  • add list.length_pos_of_one_lt_prod, generate list.length_pos_of_sum_pos using to_additive;
  • add list.length_pos_of_prod_lt_one and its additive version.

Estimated changes