Theorem Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun'

Modification history

2026-06-04 20:35

Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean

feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of `Monomial`s (#37415) …

Modified Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun'View on Github →

2026-04-24 11:28

Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean

feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Monomial` (#37411) …

Added Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun'View on Github →