Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-06-10 09:47
836c0a26
View on Github →
chore(*): use sum notation (
#3014
) The biggest field test of the new summation notation.
Estimated changes
Modified
src/algebra/big_operators.lean
modified
theorem
finset.exists_le_of_sum_le
Modified
src/algebra/direct_sum.lean
Modified
src/algebra/geom_sum.lean
Modified
src/algebra/pi_instances.lean
Modified
src/algebra/ring.lean
Modified
src/analysis/analytic/basic.lean
Modified
src/analysis/analytic/composition.lean
Modified
src/analysis/convex/basic.lean
modified
theorem
convex.sum_mem
modified
theorem
finset.center_mass_eq_of_sum_1
modified
theorem
finset.center_mass_insert
Modified
src/analysis/mean_inequalities.lean
modified
theorem
nnreal.am_gm_weighted
modified
theorem
nnreal.pow_am_le_am_pow
Modified
src/analysis/normed_space/banach.lean
Modified
src/analysis/normed_space/basic.lean
modified
theorem
nnnorm_sum_le
modified
theorem
norm_sum_le
Modified
src/analysis/normed_space/finite_dimension.lean
Modified
src/analysis/normed_space/multilinear.lean
Modified
src/analysis/specific_limits.lean
Modified
src/combinatorics/composition.lean
modified
theorem
composition.sum_blocks_fun
Modified
src/data/complex/exponential.lean
modified
def
complex.exp'
modified
theorem
complex.exp_sum
modified
theorem
complex.is_cau_exp
modified
theorem
is_cau_geo_series_const
modified
theorem
is_cau_series_of_abv_cau
modified
theorem
real.exp_sum
Modified
src/data/dfinsupp.lean
Modified
src/data/finsupp.lean
Modified
src/data/fintype/card.lean
Modified
src/data/holor.lean
Modified
src/data/indicator_function.lean
Modified
src/data/matrix/basic.lean
Modified
src/data/monoid_algebra.lean
Modified
src/data/mv_polynomial.lean
Modified
src/data/nat/multiplicity.lean
Modified
src/data/nat/totient.lean
modified
theorem
nat.sum_totient
Modified
src/data/polynomial.lean
Modified
src/data/real/cau_seq.lean
Modified
src/data/real/ennreal.lean
Modified
src/data/real/nnreal.lean
Modified
src/data/support.lean
Modified
src/field_theory/mv_polynomial.lean
Modified
src/group_theory/group_action.lean
Modified
src/group_theory/order_of_element.lean
Modified
src/group_theory/sylow.lean
Modified
src/linear_algebra/basic.lean
Modified
src/linear_algebra/basis.lean
Modified
src/linear_algebra/bilinear_form.lean
Modified
src/linear_algebra/dimension.lean
Modified
src/linear_algebra/matrix.lean
modified
theorem
matrix.trace_diag
Modified
src/linear_algebra/multilinear.lean
modified
theorem
multilinear_map.map_sum_finset_aux
Modified
src/linear_algebra/nonsingular_inverse.lean
Modified
src/measure_theory/bochner_integration.lean
Modified
src/measure_theory/giry_monad.lean
Modified
src/measure_theory/integration.lean
Modified
src/measure_theory/l1_space.lean
Modified
src/measure_theory/lebesgue_measure.lean
Modified
src/measure_theory/measure_space.lean
Modified
src/measure_theory/outer_measure.lean
Modified
src/measure_theory/probability_mass_function.lean
modified
def
pmf.of_fintype
Modified
src/measure_theory/set_integral.lean
Modified
src/number_theory/bernoulli.lean
Modified
src/number_theory/quadratic_reciprocity.lean
Modified
src/number_theory/sum_four_squares.lean
Modified
src/representation_theory/maschke.lean
Modified
src/ring_theory/adjoin_root.lean
Modified
src/ring_theory/algebra.lean
Modified
src/ring_theory/ideal_operations.lean
Modified
src/ring_theory/ideals.lean
Modified
src/ring_theory/multiplicity.lean
Modified
src/ring_theory/noetherian.lean
Modified
src/ring_theory/power_series.lean
Modified
src/ring_theory/subsemiring.lean
Modified
src/topology/algebra/infinite_sum.lean
modified
def
has_sum
modified
theorem
has_sum_fintype
modified
theorem
has_sum_sum_of_ne_finset_zero
modified
theorem
tsum_fintype
Modified
src/topology/algebra/module.lean
Modified
src/topology/algebra/multilinear.lean
Modified
src/topology/instances/ennreal.lean
Modified
src/topology/metric_space/basic.lean
Modified
src/topology/metric_space/emetric_space.lean