Def Mathlib.Meta.Positivity.evalRealCosArctan

Modification history

2025-07-31 14:34

Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

feat(Arctan): add more `simp` lemmas (#27719) …

Added Mathlib.Meta.Positivity.evalRealCosArctan View on Github →