Theorem Real.abs_cos_int_mul_pi

Modification history

2024-08-21 11:26
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
feat(Archive/Imo): formalize IMO 1961q3 (#9883)
Added Real.abs_cos_int_mul_piView on Github →