Commit 2024-08-21 11:26 8b4a3e54

View on Github →

feat(Archive/Imo): formalize IMO 1961q3 (#9883)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo1961Q3.lean

added theorem Imo1961Q3

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Real.abs_cos_int_mul_pi