Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-24 19:51 2aa08c1f

View on Github →

chore(algebra/ordered_group): merge add_le_add' with add_le_add (#3159) Also drop mul_le_mul'' (was a weaker version of mul_le_mul').

Estimated changes

Modified src/algebra/big_operators.lean

Modified src/algebra/group_power.lean

Modified src/algebra/ordered_group.lean

deleted theorem mul_le_mul''

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/enorm.lean

Modified src/data/polynomial.lean

Modified src/data/real/ennreal.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/order/filter/extr.lean

Modified src/ring_theory/polynomial.lean

Modified src/ring_theory/power_series.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/metric_space/baire.lean

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/contracting.lean

Modified src/topology/metric_space/emetric_space.lean

Modified src/topology/metric_space/hausdorff_distance.lean

Modified src/topology/metric_space/lipschitz.lean