Commit 2025-11-06 11:49 728f6683

View on Github →

chore(Analysis/SpecialFunctions/Exp): use fun_prop more (#31304) Golf a few proofs with it, and tag a few more lemmas. Noticed in passing, why not improve the tagging here?

Estimated changes

modified theorem Real.continuousOn_exp
modified theorem Real.continuous_exp