Theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_cons

Modification history

2026-04-24 11:28
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean
feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Monomial` (#37411) …
Added Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_consView on Github →