Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 13:13 7430d2d4

View on Github →

feat(data/complex/exponential): more simp lemmas (#14731) Add simp attrs and simp lemmas.

Estimated changes

Modified src/data/complex/exponential.lean

modified theorem complex.cosh_add_sinh

modified theorem complex.cosh_of_real_re

modified theorem complex.cosh_sq_sub_sinh_sq

modified theorem complex.cosh_sub_sinh

added theorem complex.exp_sub_cosh

added theorem complex.exp_sub_sinh

modified theorem complex.of_real_cosh_of_real_re

modified theorem complex.sinh_add_cosh

added theorem complex.sinh_sub_cosh

modified theorem real.cosh_add_sinh

modified theorem real.cosh_neg

added theorem real.cosh_sq'

modified theorem real.cosh_sq_sub_sinh_sq

added theorem real.cosh_sub_sinh

added theorem real.exp_sub_cosh

added theorem real.exp_sub_sinh

modified theorem real.sinh_add_cosh

added theorem real.sinh_lt_cosh

added theorem real.sinh_sub_cosh