Commit 2026-04-16 17:52 105b3705

View on Github →

feat(Tactic): algebra tactic. (#31508) Implement tactic for normalizing expressions in an algebra over a ring. Handles all of the normal ring operations as well as scalar multiplication over a fixed base ring. The core of this tactic is used by a larger suite of tactics (see #30374).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Algebra/Basic.lean

added inductive Mathlib.Tactic.Algebra.BaseType

added structure Mathlib.Tactic.Algebra.Cache

added def Mathlib.Tactic.Algebra.ExBase

added def Mathlib.Tactic.Algebra.ExProd

added def Mathlib.Tactic.Algebra.ExSum

added theorem Mathlib.Tactic.Algebra.Int.algebraMap_eq_cast

added theorem Mathlib.Tactic.Algebra.Int.cast_eq_algebraMap

added theorem Mathlib.Tactic.Algebra.Nat.algebraMap_eq_cast

added theorem Mathlib.Tactic.Algebra.Nat.cast_eq_algebraMap

added def Mathlib.Tactic.Algebra.RingCompute.add

added def Mathlib.Tactic.Algebra.RingCompute.cast

added def Mathlib.Tactic.Algebra.RingCompute.derive

added def Mathlib.Tactic.Algebra.RingCompute.inv

added def Mathlib.Tactic.Algebra.RingCompute.isOne

added def Mathlib.Tactic.Algebra.RingCompute.mul

added def Mathlib.Tactic.Algebra.RingCompute.neg

added def Mathlib.Tactic.Algebra.RingCompute.pow

added def Mathlib.Tactic.Algebra.cleanupConsts

added def Mathlib.Tactic.Algebra.cleanupSMul

added def Mathlib.Tactic.Algebra.evalCast

added def Mathlib.Tactic.Algebra.evalSMulCast

added def Mathlib.Tactic.Algebra.inferBase

added def Mathlib.Tactic.Algebra.mkCache

added def Mathlib.Tactic.Algebra.pickLargerRing

added def Mathlib.Tactic.Algebra.preprocess

added def Mathlib.Tactic.Algebra.proveEq

added def Mathlib.Tactic.Algebra.pushCast

added def Mathlib.Tactic.Algebra.ringCompare

added def Mathlib.Tactic.Algebra.ringCompute

Created Mathlib/Tactic/Algebra/Lemmas.lean

added theorem Mathlib.Tactic.Algebra.add_algebraMap

added theorem Mathlib.Tactic.Algebra.add_algebraMap_isNat_zero

added theorem Mathlib.Tactic.Algebra.add_assoc_rev

added theorem Mathlib.Tactic.Algebra.add_eq_of_add_zero

added theorem Mathlib.Tactic.Algebra.add_eq_of_eq_eq

added theorem Mathlib.Tactic.Algebra.add_eq_of_zero_add

added theorem Mathlib.Tactic.Algebra.add_eq_zero

added theorem Mathlib.Tactic.Algebra.add_neg

added theorem Mathlib.Tactic.Algebra.cast_smul_eq_mul

added theorem Mathlib.Tactic.Algebra.eq_trans_trans

added theorem Mathlib.Tactic.Algebra.int_rawCast_neg

added theorem Mathlib.Tactic.Algebra.inv_algebraMap

added theorem Mathlib.Tactic.Algebra.isInt_negOfNat_eq

added theorem Mathlib.Tactic.Algebra.isNNRat_eq_rawCast

added theorem Mathlib.Tactic.Algebra.isNat_eq_rawCast

added theorem Mathlib.Tactic.Algebra.isNat_zero_eq

added theorem Mathlib.Tactic.Algebra.isOne_algebraMap

added theorem Mathlib.Tactic.Algebra.isRat_eq_rawCast

added theorem Mathlib.Tactic.Algebra.mul_assoc_rev

added theorem Mathlib.Tactic.Algebra.mul_eq_mul_of_eq

added theorem Mathlib.Tactic.Algebra.mul_neg

added theorem Mathlib.Tactic.Algebra.nat_rawCast_0

added theorem Mathlib.Tactic.Algebra.nat_rawCast_1

added theorem Mathlib.Tactic.Algebra.nat_rawCast_2

added theorem Mathlib.Tactic.Algebra.neg_1_smul

added theorem Mathlib.Tactic.Algebra.neg_algebraMap

added theorem Mathlib.Tactic.Algebra.neg_ofNat_smul

added theorem Mathlib.Tactic.Algebra.nnRat_ofNat_smul_1

added theorem Mathlib.Tactic.Algebra.nnRat_ofNat_smul_2

added theorem Mathlib.Tactic.Algebra.nnrat_rawCast

added theorem Mathlib.Tactic.Algebra.ofNat_smul

added theorem Mathlib.Tactic.Algebra.pow_algebraMap

added theorem Mathlib.Tactic.Algebra.rat_ofNat_smul_1

added theorem Mathlib.Tactic.Algebra.rat_ofNat_smul_2

added theorem Mathlib.Tactic.Algebra.rat_rawCast_neg

added theorem Mathlib.Tactic.Algebra.smul_one_eq_smul_one'

added theorem Mathlib.Tactic.Algebra.smul_one_eq_zero

Modified Mathlib/Tactic/Ring/Common.lean

Created MathlibTest/Algebra.lean