Commit 2026-01-24 17:29 61d26a47

chore(Analysis/Complex/Trigonometric): bound Complex.sin near a cubic (#34350) We generalise the proofs of Real.cos_bound and Real.sin_bound to work in the complex numbers. We golf those two proofs to use the more general version. While tighter bounds can of course be found, we choose to stick with the existing bounds since they can be conveniently proved at this point in mathlib, and are relatively simple.