Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-11 13:26 9228ff9c

View on Github →

feat(algebra/ordered_group): abs_sub (#7850)

rename abs_sub to abs_sub_comm
prove abs_sub

Estimated changes

Modified src/algebra/continued_fractions/computation/approximation_corollaries.lean

Modified src/algebra/ordered_group.lean

modified theorem abs_sub

added theorem abs_sub_comm

Modified src/data/complex/basic.lean

deleted theorem complex.abs_sub

added theorem complex.abs_sub_comm

Modified src/data/complex/exponential.lean

Modified src/data/complex/exponential_bounds.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/geometry/euclidean/sphere.lean

Modified src/topology/algebra/ordered/basic.lean

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/uniform_space/compare_reals.lean