Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 08:06 c658f5cc

View on Github →

refactor(algebra/field): allow custom div (#6874)

Estimated changes

Modified src/algebra/field.lean

Modified src/algebra/ordered_field.lean

Modified src/analysis/asymptotics/asymptotic_equivalent.lean

Modified src/analysis/asymptotics/asymptotics.lean

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/analysis/specific_limits.lean

Modified src/data/complex/exponential.lean

Modified src/data/polynomial/denoms_clearable.lean

Modified src/data/real/cau_seq.lean

added theorem cau_seq.const_zero

Modified src/data/real/cau_seq_completion.lean

Modified src/data/set/intervals/unordered_interval.lean

Modified src/deprecated/subfield.lean

added theorem is_subfield.div_mem

Modified src/measure_theory/borel_space.lean

Modified src/order/filter/at_top_bot.lean

Modified src/ring_theory/ideal/basic.lean