Commit 2026-04-24 11:28 8cae5da4

View on Github →

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

Introduce Monomial and UnitMonomial
Define Monomial.toFun and algebraic operations on monomials: negation, inversion, multiplication.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

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

added theorem Tactic.ComputeAsymptotics.Monomial.cons_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.inv_length

added theorem Tactic.ComputeAsymptotics.Monomial.inv_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.mul_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.neg_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.nil_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.smul_toFun

added theorem Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun'

added theorem Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun

added structure Tactic.ComputeAsymptotics.Monomial

added theorem Tactic.ComputeAsymptotics.UnitMonomial.inv_length

added theorem Tactic.ComputeAsymptotics.UnitMonomial.inv_toFun

added theorem Tactic.ComputeAsymptotics.UnitMonomial.mul_length

added theorem Tactic.ComputeAsymptotics.UnitMonomial.mul_toFun

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_cons

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil_basis

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_cons

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil_basis