Commit 2024-07-19 08:06 bb5c2ab8

View on Github →

chore(Tactic/Ring/Basic): reduce use of autoImplicit (#14709)

Estimated changes

Modified Mathlib/Tactic/Ring/Basic.lean

modified def Mathlib.Tactic.Ring.ExBase.toProd

modified def Mathlib.Tactic.Ring.ExProd.coeff

modified def Mathlib.Tactic.Ring.ExProd.evalInv

modified def Mathlib.Tactic.Ring.ExProd.toSum

modified inductive Mathlib.Tactic.Ring.ExProd

modified def Mathlib.Tactic.Ring.ExSum.evalInv

modified inductive Mathlib.Tactic.Ring.ExSum

modified theorem Mathlib.Tactic.Ring.add_congr

modified theorem Mathlib.Tactic.Ring.add_mul

modified theorem Mathlib.Tactic.Ring.add_pos_left

modified theorem Mathlib.Tactic.Ring.add_pos_right

modified theorem Mathlib.Tactic.Ring.cast_neg

modified theorem Mathlib.Tactic.Ring.cast_pos

modified theorem Mathlib.Tactic.Ring.cast_rat

modified theorem Mathlib.Tactic.Ring.coeff_mul

modified theorem Mathlib.Tactic.Ring.div_pf

modified def Mathlib.Tactic.Ring.evalAddOverlap

modified def Mathlib.Tactic.Ring.evalCast

modified def Mathlib.Tactic.Ring.evalDiv

modified def Mathlib.Tactic.Ring.evalMul

modified def Mathlib.Tactic.Ring.evalMul₁

modified def Mathlib.Tactic.Ring.evalNSMul

modified def Mathlib.Tactic.Ring.evalNeg

modified def Mathlib.Tactic.Ring.evalNegProd

modified def Mathlib.Tactic.Ring.evalPow

modified def Mathlib.Tactic.Ring.evalPowAtom

modified def Mathlib.Tactic.Ring.evalPowProd

modified def Mathlib.Tactic.Ring.evalPowProdAtom

modified def Mathlib.Tactic.Ring.evalSub

modified def Mathlib.Tactic.Ring.extractCoeff

modified theorem Mathlib.Tactic.Ring.inv_add

modified theorem Mathlib.Tactic.Ring.mul_add

modified theorem Mathlib.Tactic.Ring.mul_congr

modified theorem Mathlib.Tactic.Ring.mul_exp_pos

modified theorem Mathlib.Tactic.Ring.mul_pf_left

modified theorem Mathlib.Tactic.Ring.mul_pf_right

modified theorem Mathlib.Tactic.Ring.mul_pow

modified theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap

modified theorem Mathlib.Tactic.Ring.natCast_add

modified theorem Mathlib.Tactic.Ring.natCast_mul

modified theorem Mathlib.Tactic.Ring.nsmul_congr

modified theorem Mathlib.Tactic.Ring.pow_add

modified theorem Mathlib.Tactic.Ring.pow_bit0

modified theorem Mathlib.Tactic.Ring.pow_bit1

modified theorem Mathlib.Tactic.Ring.pow_congr

modified theorem Mathlib.Tactic.Ring.pow_nat

modified theorem Mathlib.Tactic.Ring.single_pow

modified theorem Mathlib.Tactic.Ring.smul_eq_cast

modified theorem Mathlib.Tactic.Ring.smul_nat

modified theorem Mathlib.Tactic.Ring.zero_pow