Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes