Commit 2026-06-25 15:06 20711864

View on Github →

feat(Tactic): polynomial(_nf) tactics (#31513) Implement tactic for proving equality of polynomials. This tactic is part of a larger suite (see https://github.com/leanprover-community/mathlib4/pull/30374). Also generalize the preprocessing step for algebra so that it always replaces algebraMap R A r with r • 1 instead of only when R is Nat or Int. This was an oversight in algebra that broke polynomial.

depends on: #31508

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.C_eq_algebraMap

added def MvPolynomial.mvPolynomialInferBaseImpl

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Algebra/AlgebraNF.lean

added def Mathlib.Tactic.Algebra.cleanupConsts

added def Mathlib.Tactic.Algebra.cleanupSMul

Modified Mathlib/Tactic/Algebra/Basic.lean

deleted theorem Mathlib.Tactic.Algebra.Int.algebraMap_eq_cast

deleted theorem Mathlib.Tactic.Algebra.Nat.algebraMap_eq_cast

deleted def Mathlib.Tactic.Algebra.cleanupConsts

deleted def Mathlib.Tactic.Algebra.cleanupSMul

modified def Mathlib.Tactic.Algebra.preprocess

Created Mathlib/Tactic/Polynomial/Basic.lean

added def Mathlib.Tactic.Polynomial.cleanup

added def Mathlib.Tactic.Polynomial.evalExprPoly

added theorem Mathlib.Tactic.Polynomial.map_algebraMap

added theorem Mathlib.Tactic.Polynomial.monomial_eq_smul

added def Mathlib.Tactic.Polynomial.polynomialInferBase

added def Mathlib.Tactic.Polynomial.preprocess

Created Mathlib/Tactic/Polynomial/Core.lean

added structure Mathlib.Tactic.Polynomial.PolynomialExt

added def Mathlib.Tactic.Polynomial.inferBase

added def Mathlib.Tactic.Polynomial.mkPolynomialExt

Created MathlibTest/Tactic/Polynomial.lean