Theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_head

Modification history

2026-10-26 16:38
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean
chore: rename `nonzero` to `ne_zero` in theorem names (#44824) …
Deleted Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_headView on Github →
2026-06-04 20:35
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean
feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of `Monomial`s (#37415) …
Added Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_headView on Github →