Theorem Real.tan_pi_div_three

Modification history

2025-05-08 15:46
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
chore(*): use notation for `Real.sqrt` (#24684) …
Modified Real.tan_pi_div_threeView on Github →
2024-02-13 23:17
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
feat: arctangent addition and Machin's formula for π (#9847) …
Added Real.tan_pi_div_threeView on Github →