Theorem AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero

Modification history

2026-01-06 17:44
Mathlib/Analysis/Analytic/Order.lean
feat(Analysis/Analytic): analytic order of a composition (#33000) …
Added AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zeroView on Github →