Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:33 c0577580

View on Github →

feat(data/complex/exponential): exp_eq_one_iff

Estimated changes

added theorem real.exp_eq_one_iff