Commit 2020-08-13 06:22 6c8b2cd6

View on Github →

fix(algebra/field) remove one_div_eq_inv (#3749) It already existed as one_div for group_with_zero Also make one_div a simp lemma and renamed nnreal.one_div_eq_inv to nnreal.one_div.

Estimated changes

Modified src/algebra/archimedean.lean

Modified src/algebra/field.lean

deleted theorem one_div_eq_inv

Modified src/algebra/field_power.lean

Modified src/algebra/group_with_zero.lean

modified theorem one_div

modified theorem one_div_one_div

Modified src/algebra/ordered_field.lean

Modified src/analysis/analytic/basic.lean

Modified src/analysis/asymptotics.lean

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/convex/basic.lean

Modified src/analysis/mean_inequalities.lean

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/special_functions/trigonometric.lean

Modified src/analysis/specific_limits.lean

Modified src/data/complex/basic.lean

Modified src/data/complex/exponential.lean

Modified src/data/nat/cast.lean

Modified src/data/real/conjugate_exponents.lean

Modified src/data/real/hyperreal.lean

Modified src/data/real/nnreal.lean

added theorem nnreal.one_div

deleted theorem nnreal.one_div_eq_inv

Modified src/measure_theory/simple_func_dense.lean

Modified src/tactic/interactive.lean

Modified src/tactic/norm_num.lean

Modified src/topology/metric_space/pi_Lp.lean