Commit 2026-04-06 00:30 053a0031

View on Github →

refactor(Tactic): change ring to allow for coefficients in a variable type (#34734) Add a parameter to the ring normal form that allows for the coefficients to be represented by a custom BaseType. ring (roughly) sets BaseType to be Rat and implements addition/multiplication/etc. using norm_num. The changes should not be noticeable to users. Care was taken to change as little of the implementation details as possible. This refactor is made in preparation of the algebra tactic proposed in #31508. In particular algebra will (roughly) set BaseType to Ring.ExSum. This will allow algebra to share much of its internals with ring.

Estimated changes

Modified Mathlib/Tactic/Ring/Basic.lean

added def Mathlib.Tactic.Ring.ExBase.cast

added def Mathlib.Tactic.Ring.ExBase.evalIntCast

added def Mathlib.Tactic.Ring.ExBase

added def Mathlib.Tactic.Ring.ExProd.cast

added def Mathlib.Tactic.Ring.ExProd.evalIntCast

added def Mathlib.Tactic.Ring.ExProd.mkNNRat

added def Mathlib.Tactic.Ring.ExProd.mkNat

added def Mathlib.Tactic.Ring.ExProd.mkNegNNRat

added def Mathlib.Tactic.Ring.ExProd.mkNegNat

added def Mathlib.Tactic.Ring.ExProd

added def Mathlib.Tactic.Ring.ExSum.cast

added def Mathlib.Tactic.Ring.ExSum.evalIntCast

added def Mathlib.Tactic.Ring.ExSum

added theorem Mathlib.Tactic.Ring.Int.smul_eq_mul

added theorem Mathlib.Tactic.Ring.Nat.smul_eq_mul

added def Mathlib.Tactic.Ring.RatCoeff.ofResult

added def Mathlib.Tactic.Ring.RatCoeff.toResult

added theorem Mathlib.Tactic.Ring.cast_neg

added theorem Mathlib.Tactic.Ring.cast_nnrat

added theorem Mathlib.Tactic.Ring.cast_pos

added theorem Mathlib.Tactic.Ring.cast_rat

added theorem Mathlib.Tactic.Ring.cast_zero

added def Mathlib.Tactic.Ring.evalCast

added theorem Mathlib.Tactic.Ring.intCast_add

added theorem Mathlib.Tactic.Ring.intCast_mul

added theorem Mathlib.Tactic.Ring.intCast_negOfNat_Int

added theorem Mathlib.Tactic.Ring.intCast_zero

added theorem Mathlib.Tactic.Ring.natCast_add

added theorem Mathlib.Tactic.Ring.natCast_int

added theorem Mathlib.Tactic.Ring.natCast_mul

added theorem Mathlib.Tactic.Ring.natCast_nat

added theorem Mathlib.Tactic.Ring.natCast_zero

added def Mathlib.Tactic.Ring.rcℕ

added theorem Mathlib.Tactic.Ring.smul_eq_mul

Modified Mathlib/Tactic/Ring/Common.lean

deleted def Mathlib.Tactic.Ring.Cache.int

deleted def Mathlib.Tactic.Ring.Cache.nat

deleted structure Mathlib.Tactic.Ring.Cache

added def Mathlib.Tactic.Ring.Common.Cache.nat

added structure Mathlib.Tactic.Ring.Common.Cache

added def Mathlib.Tactic.Ring.Common.ExBase.toProd

added def Mathlib.Tactic.Ring.Common.ExProd.coeff

added def Mathlib.Tactic.Ring.Common.ExProd.evalInv

added def Mathlib.Tactic.Ring.Common.ExProd.toSum

added def Mathlib.Tactic.Ring.Common.ExSum.evalInv

added structure Mathlib.Tactic.Ring.Common.ExtractCoeff

added inductive Mathlib.Tactic.Ring.Common.Overlap

added structure Mathlib.Tactic.Ring.Common.Result

added structure Mathlib.Tactic.Ring.Common.RingCompare

added structure Mathlib.Tactic.Ring.Common.RingCompute

added theorem Mathlib.Tactic.Ring.Common.add_congr

added theorem Mathlib.Tactic.Ring.Common.add_mul

added theorem Mathlib.Tactic.Ring.Common.add_overlap_pf

added theorem Mathlib.Tactic.Ring.Common.add_overlap_pf_zero

added theorem Mathlib.Tactic.Ring.Common.add_pf_add_gt

added theorem Mathlib.Tactic.Ring.Common.add_pf_add_lt

added theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap

added theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero

added theorem Mathlib.Tactic.Ring.Common.add_pf_add_zero

added theorem Mathlib.Tactic.Ring.Common.add_pf_zero_add

added theorem Mathlib.Tactic.Ring.Common.add_pos_left

added theorem Mathlib.Tactic.Ring.Common.add_pos_right

added theorem Mathlib.Tactic.Ring.Common.atom_pf'

added theorem Mathlib.Tactic.Ring.Common.atom_pf

added theorem Mathlib.Tactic.Ring.Common.coeff_mul

added theorem Mathlib.Tactic.Ring.Common.coeff_one

added theorem Mathlib.Tactic.Ring.Common.const_pos

added theorem Mathlib.Tactic.Ring.Common.div_congr

added theorem Mathlib.Tactic.Ring.Common.div_pf

added def Mathlib.Tactic.Ring.Common.evalAddOverlap

added def Mathlib.Tactic.Ring.Common.evalAtom

added def Mathlib.Tactic.Ring.Common.evalDiv

added def Mathlib.Tactic.Ring.Common.evalInvAtom

added def Mathlib.Tactic.Ring.Common.evalMul

added def Mathlib.Tactic.Ring.Common.evalMul₁

added def Mathlib.Tactic.Ring.Common.evalNeg

added def Mathlib.Tactic.Ring.Common.evalNegProd

added def Mathlib.Tactic.Ring.Common.evalPow

added def Mathlib.Tactic.Ring.Common.evalPowAtom

added def Mathlib.Tactic.Ring.Common.evalPowProd

added def Mathlib.Tactic.Ring.Common.evalPowProdAtom

added def Mathlib.Tactic.Ring.Common.evalSub

added def Mathlib.Tactic.Ring.Common.extractCoeff

added theorem Mathlib.Tactic.Ring.Common.inv_add

added theorem Mathlib.Tactic.Ring.Common.inv_congr

added theorem Mathlib.Tactic.Ring.Common.inv_mul

added theorem Mathlib.Tactic.Ring.Common.inv_single

added def Mathlib.Tactic.Ring.Common.isAtomOrDerivable

added def Mathlib.Tactic.Ring.Common.mkCache

added theorem Mathlib.Tactic.Ring.Common.mul_add

added theorem Mathlib.Tactic.Ring.Common.mul_congr

added theorem Mathlib.Tactic.Ring.Common.mul_exp_pos

added theorem Mathlib.Tactic.Ring.Common.mul_one

added theorem Mathlib.Tactic.Ring.Common.mul_pf_left

added theorem Mathlib.Tactic.Ring.Common.mul_pf_right

added theorem Mathlib.Tactic.Ring.Common.mul_pow

added theorem Mathlib.Tactic.Ring.Common.mul_pow_mul

added theorem Mathlib.Tactic.Ring.Common.mul_pp_pf_overlap

added theorem Mathlib.Tactic.Ring.Common.mul_zero

added theorem Mathlib.Tactic.Ring.Common.neg_add

added theorem Mathlib.Tactic.Ring.Common.neg_congr

added theorem Mathlib.Tactic.Ring.Common.neg_mul

added theorem Mathlib.Tactic.Ring.Common.neg_one_mul

added theorem Mathlib.Tactic.Ring.Common.neg_zero

added theorem Mathlib.Tactic.Ring.Common.nsmul_congr

added theorem Mathlib.Tactic.Ring.Common.one_mul

added theorem Mathlib.Tactic.Ring.Common.one_pow

added theorem Mathlib.Tactic.Ring.Common.pow_add

added theorem Mathlib.Tactic.Ring.Common.pow_atom

added theorem Mathlib.Tactic.Ring.Common.pow_bit0

added theorem Mathlib.Tactic.Ring.Common.pow_bit1

added theorem Mathlib.Tactic.Ring.Common.pow_congr

added theorem Mathlib.Tactic.Ring.Common.pow_nat

added theorem Mathlib.Tactic.Ring.Common.pow_one

added theorem Mathlib.Tactic.Ring.Common.pow_one_cast

added theorem Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat

added theorem Mathlib.Tactic.Ring.Common.pow_prod_atom

added theorem Mathlib.Tactic.Ring.Common.pow_zero

added theorem Mathlib.Tactic.Ring.Common.single_pow

added theorem Mathlib.Tactic.Ring.Common.smul_congr

added theorem Mathlib.Tactic.Ring.Common.sub_congr

added theorem Mathlib.Tactic.Ring.Common.sub_pf

added def Mathlib.Tactic.Ring.Common.sℕ

added theorem Mathlib.Tactic.Ring.Common.toProd_pf

added theorem Mathlib.Tactic.Ring.Common.zero_mul

added theorem Mathlib.Tactic.Ring.Common.zero_pow

added theorem Mathlib.Tactic.Ring.Common.zsmul_congr

deleted def Mathlib.Tactic.Ring.ExBase.cast

deleted def Mathlib.Tactic.Ring.ExBase.cmp

deleted def Mathlib.Tactic.Ring.ExBase.eq

deleted def Mathlib.Tactic.Ring.ExBase.toProd

deleted def Mathlib.Tactic.Ring.ExProd.cast

deleted def Mathlib.Tactic.Ring.ExProd.cmp

deleted def Mathlib.Tactic.Ring.ExProd.coeff

deleted def Mathlib.Tactic.Ring.ExProd.eq

deleted def Mathlib.Tactic.Ring.ExProd.evalInv

deleted def Mathlib.Tactic.Ring.ExProd.mkNNRat

deleted def Mathlib.Tactic.Ring.ExProd.mkNat

deleted def Mathlib.Tactic.Ring.ExProd.mkNegNNRat

deleted def Mathlib.Tactic.Ring.ExProd.mkNegNat

deleted def Mathlib.Tactic.Ring.ExProd.toSum

deleted def Mathlib.Tactic.Ring.ExSum.cast

deleted def Mathlib.Tactic.Ring.ExSum.cmp

deleted def Mathlib.Tactic.Ring.ExSum.eq

deleted def Mathlib.Tactic.Ring.ExSum.evalInv

deleted structure Mathlib.Tactic.Ring.ExtractCoeff

deleted inductive Mathlib.Tactic.Ring.Overlap

added structure Mathlib.Tactic.Ring.RatCoeff

deleted structure Mathlib.Tactic.Ring.Result

deleted theorem Mathlib.Tactic.Ring.add_congr

deleted theorem Mathlib.Tactic.Ring.add_mul

deleted theorem Mathlib.Tactic.Ring.add_overlap_pf

deleted theorem Mathlib.Tactic.Ring.add_overlap_pf_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_add_gt

deleted theorem Mathlib.Tactic.Ring.add_pf_add_lt

deleted theorem Mathlib.Tactic.Ring.add_pf_add_overlap

deleted theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_add_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_zero_add

deleted theorem Mathlib.Tactic.Ring.add_pos_left

deleted theorem Mathlib.Tactic.Ring.add_pos_right

deleted theorem Mathlib.Tactic.Ring.atom_pf'

deleted theorem Mathlib.Tactic.Ring.atom_pf

deleted theorem Mathlib.Tactic.Ring.cast_neg

deleted theorem Mathlib.Tactic.Ring.cast_nnrat

deleted theorem Mathlib.Tactic.Ring.cast_pos

deleted theorem Mathlib.Tactic.Ring.cast_rat

deleted theorem Mathlib.Tactic.Ring.cast_zero

deleted theorem Mathlib.Tactic.Ring.coeff_mul

deleted theorem Mathlib.Tactic.Ring.coeff_one

deleted theorem Mathlib.Tactic.Ring.const_pos

deleted theorem Mathlib.Tactic.Ring.div_congr

deleted theorem Mathlib.Tactic.Ring.div_pf

deleted def Mathlib.Tactic.Ring.evalAddOverlap

deleted def Mathlib.Tactic.Ring.evalAtom

deleted def Mathlib.Tactic.Ring.evalCast

deleted def Mathlib.Tactic.Ring.evalDiv

deleted def Mathlib.Tactic.Ring.evalInvAtom

deleted def Mathlib.Tactic.Ring.evalMul

deleted def Mathlib.Tactic.Ring.evalMul₁

deleted def Mathlib.Tactic.Ring.evalNSMul

deleted def Mathlib.Tactic.Ring.evalNeg

deleted def Mathlib.Tactic.Ring.evalNegProd

deleted def Mathlib.Tactic.Ring.evalPow

deleted def Mathlib.Tactic.Ring.evalPowAtom

deleted def Mathlib.Tactic.Ring.evalPowProd

deleted def Mathlib.Tactic.Ring.evalPowProdAtom

deleted def Mathlib.Tactic.Ring.evalSub

deleted def Mathlib.Tactic.Ring.evalZSMul

deleted def Mathlib.Tactic.Ring.extractCoeff

deleted theorem Mathlib.Tactic.Ring.intCast_add

deleted theorem Mathlib.Tactic.Ring.intCast_mul

deleted theorem Mathlib.Tactic.Ring.intCast_negOfNat_Int

deleted theorem Mathlib.Tactic.Ring.intCast_zero

deleted theorem Mathlib.Tactic.Ring.inv_add

deleted theorem Mathlib.Tactic.Ring.inv_congr

deleted theorem Mathlib.Tactic.Ring.inv_mul

deleted theorem Mathlib.Tactic.Ring.inv_single

deleted def Mathlib.Tactic.Ring.isAtomOrDerivable

deleted def Mathlib.Tactic.Ring.mkCache

deleted theorem Mathlib.Tactic.Ring.mul_add

deleted theorem Mathlib.Tactic.Ring.mul_congr

deleted theorem Mathlib.Tactic.Ring.mul_exp_pos

deleted theorem Mathlib.Tactic.Ring.mul_one

deleted theorem Mathlib.Tactic.Ring.mul_pf_left

deleted theorem Mathlib.Tactic.Ring.mul_pf_right

deleted theorem Mathlib.Tactic.Ring.mul_pow

deleted theorem Mathlib.Tactic.Ring.mul_pow_mul

deleted theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap

deleted theorem Mathlib.Tactic.Ring.mul_zero

deleted theorem Mathlib.Tactic.Ring.natCast_add

deleted theorem Mathlib.Tactic.Ring.natCast_int

deleted theorem Mathlib.Tactic.Ring.natCast_mul

deleted theorem Mathlib.Tactic.Ring.natCast_nat

deleted theorem Mathlib.Tactic.Ring.natCast_zero

deleted theorem Mathlib.Tactic.Ring.neg_add

deleted theorem Mathlib.Tactic.Ring.neg_congr

deleted theorem Mathlib.Tactic.Ring.neg_mul

deleted theorem Mathlib.Tactic.Ring.neg_one_mul

deleted theorem Mathlib.Tactic.Ring.neg_zero

deleted theorem Mathlib.Tactic.Ring.nsmul_congr

deleted theorem Mathlib.Tactic.Ring.one_mul

deleted theorem Mathlib.Tactic.Ring.one_pow

deleted theorem Mathlib.Tactic.Ring.pow_add

deleted theorem Mathlib.Tactic.Ring.pow_atom

deleted theorem Mathlib.Tactic.Ring.pow_bit0

deleted theorem Mathlib.Tactic.Ring.pow_bit1

deleted theorem Mathlib.Tactic.Ring.pow_congr

deleted theorem Mathlib.Tactic.Ring.pow_nat

deleted theorem Mathlib.Tactic.Ring.pow_one

deleted theorem Mathlib.Tactic.Ring.pow_one_cast

deleted theorem Mathlib.Tactic.Ring.pow_prod_atom

deleted theorem Mathlib.Tactic.Ring.pow_zero

deleted theorem Mathlib.Tactic.Ring.single_pow

deleted theorem Mathlib.Tactic.Ring.smul_eq_cast

deleted theorem Mathlib.Tactic.Ring.smul_eq_intCast

deleted theorem Mathlib.Tactic.Ring.smul_int

deleted theorem Mathlib.Tactic.Ring.smul_nat

deleted theorem Mathlib.Tactic.Ring.sub_congr

deleted theorem Mathlib.Tactic.Ring.sub_pf

deleted def Mathlib.Tactic.Ring.sℕ

deleted def Mathlib.Tactic.Ring.sℤ

deleted theorem Mathlib.Tactic.Ring.toProd_pf

deleted theorem Mathlib.Tactic.Ring.zero_mul

deleted theorem Mathlib.Tactic.Ring.zero_pow

deleted theorem Mathlib.Tactic.Ring.zsmul_congr

Modified Mathlib/Tactic/Ring/Compare.lean

Modified Mathlib/Tactic/Ring/RingNF.lean

deleted def Mathlib.Tactic.Ring.ExBase.isAtom

deleted def Mathlib.Tactic.Ring.ExProd.isAtom

deleted def Mathlib.Tactic.Ring.ExSum.isAtom

Modified MathlibTest/ring.lean

Modified scripts/noshake.json