Theorem Real.two_mul_sin_mul_sin

Modification history

2025-01-27 13:29

Mathlib/Data/Complex/Exponential.lean

chore(Data/Complex/Exponential): split trig functions to new file (#21075) …

Modified Real.two_mul_sin_mul_sin View on Github →

2024-11-13 21:29

Mathlib/Data/Complex/Exponential.lean

feat(Archive/Imo): IMO 1963 Q5 (#18789) …

Added Real.two_mul_sin_mul_sin View on Github →