Commit 2025-01-27 13:29 e779c77e
View on Github →chore(Data/Complex/Exponential): split trig functions to new file (#21075) This PR splits Data/Complex/Exponential.lean into a new Trigonometric.lean file, addressing an instance of a long file linter trigger.