Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-06 17:03 14a19bf3

View on Github →

fix(*): update to lean Adding typeclasses to the context must now be done with haveI, introsI, etc.

Estimated changes

Modified algebra/archimedean.lean

Modified algebra/big_operators.lean

Modified algebra/field.lean

Modified algebra/linear_algebra/linear_map_module.lean

Modified algebra/linear_algebra/subtype_module.lean

Modified algebra/module.lean

modified theorem one_smul

Modified analysis/metric_space.lean

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/topological_structures.lean

Modified analysis/topology/uniform_space.lean

added def uniform_space.mk'

Modified data/analysis/filter.lean

Modified data/analysis/topology.lean

Modified data/finset.lean

Modified data/fintype.lean

Modified data/list/basic.lean

Modified data/list/perm.lean

Modified data/nat/basic.lean

Modified data/num/lemmas.lean

Modified data/real/cau_seq.lean

Modified data/seq/computation.lean

Modified data/seq/parallel.lean

Modified data/set/countable.lean

Modified data/set/finite.lean

Modified data/sum.lean

Modified logic/basic.lean

Modified logic/embedding.lean

Modified order/basic.lean

Modified order/order_iso.lean

Modified set_theory/cardinal.lean

Modified set_theory/cofinality.lean

Modified set_theory/ordinal.lean

Modified set_theory/ordinal_notation.lean

Modified set_theory/zfc.lean

Modified tactic/basic.lean

Modified tactic/interactive.lean

Modified tactic/rcases.lean