Commit 2020-08-21 11:41 4921be9d
View on Github →feat(analysis/special_functions/arsinh): inverse hyperbolic sine function (#3801)
Added the following lemmas and definitions:
cosh_def
sinh_def
cosh_pos
sinh_strict_mono
sinh_injective
sinh_surjective
sinh_bijective
real.cosh_sq_sub_sinh_sq
sqrt_one_add_sinh_sq
sinh_arsinh
arsinh_sin
This is from the list of UG not in lean. cosh coming soon.