Theorem Tactic.ComputeAsymptotics.Monomial.mul_toFun

Modification history

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