Commit 2022-10-21 17:19 b1a619c0
View on Github →refactor(analysis/special_functions/trigonometric/inverse): cos_arcsin, sin_arccos degenerate cases (#17026)
The definitions of arcsin, arccos and sqrt in degenerate cases mean that the lemmas cos_arcsin and sin_arccos are actually true for all real arguments (including those outside the interval from -1 to 1), without needing any inequality hypotheses.  Remove those inequality hypotheses from the lemmas, so simplifying use of those lemmas elsewhere.