Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-11 11:41 cf0c6b83

View on Github →

chore(*): use prod and sum notation (#3027)

Estimated changes

Modified src/algebra/big_operators.lean

modified theorem finset.prod_Ico_id_eq_fact

modified theorem finset.prod_mul_distrib

Modified src/algebra/pi_instances.lean

Modified src/analysis/analytic/composition.lean

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/iterated_deriv.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/multilinear.lean

modified theorem continuous_multilinear_map.bound

modified theorem continuous_multilinear_map.le_op_norm

modified theorem continuous_multilinear_map.norm_def

modified def continuous_multilinear_map.op_norm

modified theorem continuous_multilinear_map.op_norm_le_bound

modified theorem continuous_multilinear_map.ratio_le_op_norm

modified theorem multilinear_map.continuous_of_bound

modified def multilinear_map.mk_continuous

Modified src/data/complex/exponential.lean

modified theorem complex.exp_sum

modified theorem real.exp_sum

Modified src/data/dfinsupp.lean

Modified src/data/finsupp.lean

Modified src/data/fintype/card.lean

modified theorem fin.prod_univ_zero

Modified src/data/monoid_algebra.lean

Modified src/data/mv_polynomial.lean

modified theorem mv_polynomial.as_sum

modified theorem mv_polynomial.support_sum_monomial_coeff

Modified src/data/real/nnreal.lean

Modified src/data/set/finite.lean

Modified src/deprecated/submonoid.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/subgroup.lean

Modified src/group_theory/submonoid.lean

Modified src/linear_algebra/determinant.lean

modified theorem matrix.det_diagonal

Modified src/linear_algebra/multilinear.lean

Modified src/measure_theory/borel_space.lean

Modified src/ring_theory/subsemiring.lean

Modified src/topology/algebra/monoid.lean

Modified src/topology/algebra/multilinear.lean