Commit 2023-09-05 10:32 a1fd072e

View on Github →

chore: minimize imports in NormNum.Core (#6953) Reducing the imports in Mathlib.Tactic.NormNum.Core a bit. (I was thinking about whether it might be possible to upstream some of norm_num. As is it has a lot of prerequisites!)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

Created Mathlib/Tactic/NormNum/CharZero.lean

added def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne

added def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?

added def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing

added def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing?

added def Mathlib.Meta.NormNum.inferCharZeroOfRing

added def Mathlib.Meta.NormNum.inferCharZeroOfRing?

Modified Mathlib/Tactic/NormNum/Core.lean

deleted def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne

deleted def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?

deleted def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing

deleted def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing?

deleted def Mathlib.Meta.NormNum.inferCharZeroOfRing

deleted def Mathlib.Meta.NormNum.inferCharZeroOfRing?

deleted def Mathlib.Meta.NormNum.inferLinearOrderedField

deleted def Mathlib.Meta.NormNum.inferOrderedRing

deleted def Mathlib.Meta.NormNum.inferOrderedSemiring

deleted def Mathlib.Meta.NormNum.instDivisionRingRat

deleted def Mathlib.Meta.NormNum.instRingInt

deleted def Mathlib.Meta.NormNum.instRingRat

Created Mathlib/Tactic/NormNum/OrderedRing.lean

added def Mathlib.Meta.NormNum.inferLinearOrderedField

added def Mathlib.Meta.NormNum.inferOrderedRing

added def Mathlib.Meta.NormNum.inferOrderedSemiring

Modified Mathlib/Tactic/Positivity/Basic.lean

Modified Mathlib/Tactic/Positivity/Core.lean