Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-02 00:36 409ea425

View on Github →

chore(algebra/*): move some lemmas to div_inv_monoid (#5552)

Estimated changes

Modified src/algebra/field.lean

deleted theorem mul_div_assoc'

Modified src/algebra/group/basic.lean

added theorem mul_div_assoc'

added theorem mul_div_assoc

added theorem one_div

deleted theorem zero_sub

Modified src/algebra/group_with_zero/basic.lean

deleted theorem mul_div_assoc

deleted theorem one_div

Modified src/analysis/analytic/composition.lean

Modified src/data/complex/exponential.lean

Modified src/data/real/hyperreal.lean

Modified src/geometry/euclidean/monge_point.lean