Commit 2020-10-05 07:39 581b1415

View on Github →

feat(data/complex): norm_cast lemmas (#4405) Mark various existing lemmas such as abs_of_real and of_real_exp as norm_cast lemmas so that norm_cast and related tactics can handle expressions involving those functions, and add lemmas of_real_prod and of_real_sum to allow those tactics to work with sums and products involving coercions from real to complex.

Estimated changes

Modified src/data/complex/basic.lean

modified theorem complex.abs_of_real

added theorem complex.of_real_prod

added theorem complex.of_real_sum

Modified src/data/complex/exponential.lean

modified theorem complex.of_real_cos

modified theorem complex.of_real_cosh

modified theorem complex.of_real_exp

modified theorem complex.of_real_sin

modified theorem complex.of_real_sinh

modified theorem complex.of_real_tan

modified theorem complex.of_real_tanh