Commit 2026-10-19 09:27 02aea1d0

View on Github →

fix(Analysis/Trigonometric): relax unnecessary condition on Euler product for sine (#45015) Discovered while reviewing #45014. I also have opinions on the location and naming of these lemmas (my hot take is the definition sineTerm shouldn't exist and it should be inlined everywhere), but those needs import shuffling and possibly renaming quite a lot of stuff, so let me start with the least controversial move here.

Estimated changes