inverse): `tan_arcsin`, `tan_arccos`, `arccos_eq_arcsin`, `arcsin_eq_arccos` (#17105)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/inverse): `tan_arcsin`, `tan_arccos`, `arccos_eq_arcsin`, `arcsin_eq_arccos` (#17105) Add four more lemmas involving `arcsin` and `arccos`, analogous to lemmas already present.

Author

jsm28

Parents

23ffd4ac

mathlib3 cc26a6cb - feat(analysis/special_functions/trigonometric/inverse): `tan_arcsin`, `tan_arccos`, `arccos_eq_arcsin`, `arcsin_eq_arccos` (#17105)

mathlib3
cc26a6cb - feat(analysis/special_functions/trigonometric/inverse): `tan_arcsin`, `tan_arccos`, `arccos_eq_arcsin`, `arcsin_eq_arccos` (#17105)