Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 06:39 c1edbdda

View on Github →

chore(data/complex/exponential): golf 2 proofs (#5126)

Estimated changes

Modified src/algebra/ordered_ring.lean

added theorem abs_le_one_iff_mul_self_le_one

Modified src/data/complex/exponential.lean