Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-05 11:24 f6474f0c

View on Github →

chore(.): adapt to change b7322e28c12d274ccec992b7fc49d35b2e56a2a4 (remove AC simp rules)

Estimated changes

Modified algebra/field.lean

Modified algebra/group_power.lean

Modified algebra/module.lean

Modified algebra/ring.lean

Modified analysis/ennreal.lean

Modified analysis/limits.lean

Modified analysis/measure_theory/borel_space.lean

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/metric_space.lean

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

Modified analysis/topology/uniform_space.lean

Modified data/analysis/filter.lean

Modified data/analysis/topology.lean

Modified data/array/lemmas.lean

Modified data/finset.lean

modified def finset.fold

Modified data/hash_map.lean

Modified data/list/basic.lean

modified theorem list.diff_nil

modified theorem list.pw_filter_nil

Modified data/list/perm.lean

Modified data/list/sort.lean

Modified data/multiset.lean

added theorem multiset.quot_mk_to_coe''

Modified data/nat/basic.lean

Modified data/nat/gcd.lean

Modified data/nat/modeq.lean

Modified data/nat/sqrt.lean

Modified data/num/lemmas.lean

Modified data/rat.lean

Modified data/seq/wseq.lean

Modified data/set/basic.lean

Modified data/set/countable.lean

Modified data/set/finite.lean

Modified data/set/lattice.lean

Modified data/set/prod.lean

Modified logic/basic.lean

Modified order/complete_lattice.lean

Modified order/filter.lean

Modified order/zorn.lean

Modified pending/default.lean

added theorem of_to_bool_iff

Modified tactic/finish.lean

Modified tests/finish3.lean

Modified theories/number_theory/dioph.lean

modified theorem dioph.dioph_comp

modified theorem dioph.dioph_fn_comp

Modified theories/number_theory/pell.lean

Modified theories/set_theory.lean