Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-30 06:58 0b476751

View on Github →

feat(algebra,data/complex/exponential): add abs_neg_one_pow, remove hyp from div_le_div_of_le_left (#1280)

Estimated changes

Modified src/algebra/field.lean

modified theorem inv_eq_zero

Modified src/algebra/group_power.lean

added theorem abs_neg_one_pow

Modified src/algebra/ordered_field.lean

modified theorem div_le_div_of_le_left

Modified src/data/complex/exponential.lean