Commit 2025-04-23 09:35 c8ed5874
View on Github →feat(Analysis/Analytic): characterization of order (#24256)
Alternative characterization of the order of vanishing of analytic functions which avoids case splits on ENat. Also golf a proof using filter_upwards.