Theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil_basis

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.toFun_nil_basisView on Github →