Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-07 03:42 60d14579

View on Github →

chore(algebra/big_operators): drop some decidable_eq assumptions (#2332)

  • chore(algebra/big_operators): drop some decidable_eq assumptions I wonder why lint didn't report them.
  • Drop unused arguments

Estimated changes

modified theorem finset.prod_comm
modified theorem finset.prod_sum
modified theorem finset.prod_union_inter
modified theorem finset.filter_and
modified theorem finset.filter_not
modified theorem finset.filter_or
modified theorem matrix.mul_to_lin
modified theorem matrix.rank_vec_mul_vec
modified theorem matrix.trace_mul_comm
modified theorem matrix.trace_transpose_mul