Theorem AnalyticAt.order_add

Modification history

2025-05-14 13:17

Mathlib/Analysis/Analytic/Order.lean

refactor: use a junk value for the analytic order of a non-analytic function (#22974) …

Deleted AnalyticAt.order_add View on Github →

2025-04-28 06:28

Mathlib/Analysis/Analytic/Order.lean

feat: behavior of AnalyticAt.order under addition (#22680) …

Added AnalyticAt.order_add View on Github →