Commit 2026-02-04 23:34 ba07a5d5

View on Github →

refactor(Tactic/Ring): move most ring code into Common.lean (#34837) This is in preparation of #34734, which generalizes the code in Ring/Common for use in the coming algebra tactic. Moving the core of ring to Common makes the diff of said PR significantly more readable, as requested by @Vierkantor here Unfortunately a couple of the functions moved to Ring/Common will have to be moved back to Ring/Basic as they are specific to ring. These are namely the sections for n/zsmul and evalCast. They can't stay in Ring/Basic since eval depends on them.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Ring/Basic.lean

deleted def Mathlib.Tactic.Ring.Cache.int

deleted def Mathlib.Tactic.Ring.Cache.nat

deleted structure Mathlib.Tactic.Ring.Cache

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 inductive Mathlib.Tactic.Ring.ExBase

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 inductive Mathlib.Tactic.Ring.ExProd

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 inductive Mathlib.Tactic.Ring.ExSum

deleted structure Mathlib.Tactic.Ring.ExtractCoeff

deleted inductive Mathlib.Tactic.Ring.Overlap

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 def Mathlib.Tactic.Ring.instCommSemiringInt

deleted def Mathlib.Tactic.Ring.instCommSemiringNat

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_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

Created Mathlib/Tactic/Ring/Common.lean

added def Mathlib.Tactic.Ring.Cache.int

added def Mathlib.Tactic.Ring.Cache.nat

added structure Mathlib.Tactic.Ring.Cache

added def Mathlib.Tactic.Ring.ExBase.cast

added def Mathlib.Tactic.Ring.ExBase.cmp

added def Mathlib.Tactic.Ring.ExBase.eq

added def Mathlib.Tactic.Ring.ExBase.toProd

added inductive Mathlib.Tactic.Ring.ExBase

added def Mathlib.Tactic.Ring.ExProd.cast

added def Mathlib.Tactic.Ring.ExProd.cmp

added def Mathlib.Tactic.Ring.ExProd.coeff

added def Mathlib.Tactic.Ring.ExProd.eq

added def Mathlib.Tactic.Ring.ExProd.evalInv

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.toSum

added inductive Mathlib.Tactic.Ring.ExProd

added def Mathlib.Tactic.Ring.ExSum.cast

added def Mathlib.Tactic.Ring.ExSum.cmp

added def Mathlib.Tactic.Ring.ExSum.eq

added def Mathlib.Tactic.Ring.ExSum.evalInv

added inductive Mathlib.Tactic.Ring.ExSum

added structure Mathlib.Tactic.Ring.ExtractCoeff

added inductive Mathlib.Tactic.Ring.Overlap

added structure Mathlib.Tactic.Ring.Result

added theorem Mathlib.Tactic.Ring.add_congr

added theorem Mathlib.Tactic.Ring.add_mul

added theorem Mathlib.Tactic.Ring.add_overlap_pf

added theorem Mathlib.Tactic.Ring.add_overlap_pf_zero

added theorem Mathlib.Tactic.Ring.add_pf_add_gt

added theorem Mathlib.Tactic.Ring.add_pf_add_lt

added theorem Mathlib.Tactic.Ring.add_pf_add_overlap

added theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero

added theorem Mathlib.Tactic.Ring.add_pf_add_zero

added theorem Mathlib.Tactic.Ring.add_pf_zero_add

added theorem Mathlib.Tactic.Ring.add_pos_left

added theorem Mathlib.Tactic.Ring.add_pos_right

added theorem Mathlib.Tactic.Ring.atom_pf'

added theorem Mathlib.Tactic.Ring.atom_pf

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 theorem Mathlib.Tactic.Ring.coeff_mul

added theorem Mathlib.Tactic.Ring.coeff_one

added theorem Mathlib.Tactic.Ring.const_pos

added theorem Mathlib.Tactic.Ring.div_congr

added theorem Mathlib.Tactic.Ring.div_pf

added def Mathlib.Tactic.Ring.evalAddOverlap

added def Mathlib.Tactic.Ring.evalAtom

added def Mathlib.Tactic.Ring.evalCast

added def Mathlib.Tactic.Ring.evalDiv

added def Mathlib.Tactic.Ring.evalInvAtom

added def Mathlib.Tactic.Ring.evalMul

added def Mathlib.Tactic.Ring.evalMul₁

added def Mathlib.Tactic.Ring.evalNSMul

added def Mathlib.Tactic.Ring.evalNeg

added def Mathlib.Tactic.Ring.evalNegProd

added def Mathlib.Tactic.Ring.evalPow

added def Mathlib.Tactic.Ring.evalPowAtom

added def Mathlib.Tactic.Ring.evalPowProd

added def Mathlib.Tactic.Ring.evalPowProdAtom

added def Mathlib.Tactic.Ring.evalSub

added def Mathlib.Tactic.Ring.evalZSMul

added def Mathlib.Tactic.Ring.extractCoeff

added def Mathlib.Tactic.Ring.instCommSemiringInt

added def Mathlib.Tactic.Ring.instCommSemiringNat

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.inv_add

added theorem Mathlib.Tactic.Ring.inv_congr

added theorem Mathlib.Tactic.Ring.inv_mul

added theorem Mathlib.Tactic.Ring.inv_single

added def Mathlib.Tactic.Ring.isAtomOrDerivable

added def Mathlib.Tactic.Ring.mkCache

added theorem Mathlib.Tactic.Ring.mul_add

added theorem Mathlib.Tactic.Ring.mul_congr

added theorem Mathlib.Tactic.Ring.mul_exp_pos

added theorem Mathlib.Tactic.Ring.mul_one

added theorem Mathlib.Tactic.Ring.mul_pf_left

added theorem Mathlib.Tactic.Ring.mul_pf_right

added theorem Mathlib.Tactic.Ring.mul_pow

added theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap

added theorem Mathlib.Tactic.Ring.mul_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 theorem Mathlib.Tactic.Ring.neg_add

added theorem Mathlib.Tactic.Ring.neg_congr

added theorem Mathlib.Tactic.Ring.neg_mul

added theorem Mathlib.Tactic.Ring.neg_one_mul

added theorem Mathlib.Tactic.Ring.neg_zero

added theorem Mathlib.Tactic.Ring.nsmul_congr

added theorem Mathlib.Tactic.Ring.one_mul

added theorem Mathlib.Tactic.Ring.one_pow

added theorem Mathlib.Tactic.Ring.pow_add

added theorem Mathlib.Tactic.Ring.pow_atom

added theorem Mathlib.Tactic.Ring.pow_bit0

added theorem Mathlib.Tactic.Ring.pow_bit1

added theorem Mathlib.Tactic.Ring.pow_congr

added theorem Mathlib.Tactic.Ring.pow_nat

added theorem Mathlib.Tactic.Ring.pow_one

added theorem Mathlib.Tactic.Ring.pow_one_cast

added theorem Mathlib.Tactic.Ring.pow_prod_atom

added theorem Mathlib.Tactic.Ring.pow_zero

added theorem Mathlib.Tactic.Ring.single_pow

added theorem Mathlib.Tactic.Ring.smul_eq_cast

added theorem Mathlib.Tactic.Ring.smul_eq_intCast

added theorem Mathlib.Tactic.Ring.smul_int

added theorem Mathlib.Tactic.Ring.smul_nat

added theorem Mathlib.Tactic.Ring.sub_congr

added theorem Mathlib.Tactic.Ring.sub_pf

added def Mathlib.Tactic.Ring.sℕ

added def Mathlib.Tactic.Ring.sℤ

added theorem Mathlib.Tactic.Ring.toProd_pf

added theorem Mathlib.Tactic.Ring.zero_mul

added theorem Mathlib.Tactic.Ring.zero_pow

added theorem Mathlib.Tactic.Ring.zsmul_congr