Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-25 10:39 f77cb57f

View on Github →

chore(data/fintype): move results depending on big_operators (#2044)

Estimated changes

Modified src/algebra/big_operators.lean

Modified src/analysis/normed_space/multilinear.lean

Modified src/data/fintype.lean

deleted theorem card_vector

deleted theorem fin.prod_univ_cast_succ

deleted theorem fin.prod_univ_succ

deleted theorem fin.prod_univ_zero

deleted theorem fin.sum_univ_cast_succ

deleted theorem fin.sum_univ_succ

deleted theorem finset.prod_attach_univ

deleted theorem finset.range_prod_eq_univ_prod

deleted theorem fintype.card_eq_sum_ones

deleted theorem fintype.card_fun

deleted theorem fintype.card_pi

deleted theorem fintype.card_sigma

deleted theorem fintype.card_sum

Created src/data/fintype/card.lean

added theorem card_vector

added theorem fin.prod_univ_cast_succ

added theorem fin.prod_univ_succ

added theorem fin.prod_univ_zero

added theorem fin.sum_univ_cast_succ

added theorem fin.sum_univ_succ

added theorem finset.prod_attach_univ

added theorem finset.range_prod_eq_univ_prod

added theorem fintype.card_eq_sum_ones

added theorem fintype.card_fun

added theorem fintype.card_pi

added theorem fintype.card_sigma

added theorem fintype.card_sum

Modified src/data/set/finite.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/sylow.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/determinant.lean

Modified src/number_theory/bernoulli.lean

Modified src/set_theory/cardinal.lean