Commit 2024-02-05 13:02 65a5eadc

View on Github →

chore: Move positivity extensions (#10140) The goal here is to have access to positivity earlier in the import hierarchy

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

Modified Mathlib/Algebra/Order/Archimedean.lean

Modified Mathlib/Algebra/Order/Chebyshev.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

added def Mathlib.Meta.Positivity.evalDiv

added def Mathlib.Meta.Positivity.evalInv

added def Mathlib.Meta.Positivity.evalPowZeroInt

Modified Mathlib/Algebra/Order/Field/Power.lean

added def Mathlib.Meta.Positivity.evalZPow

Modified Mathlib/Analysis/Convex/Mul.lean

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

Modified Mathlib/Data/Rat/Cast/Order.lean

added def Mathlib.Meta.Positivity.evalRatCast

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/SetTheory/Surreal/Dyadic.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

deleted def Mathlib.Meta.Positivity.evalDiv

deleted def Mathlib.Meta.Positivity.evalInv

deleted def Mathlib.Meta.Positivity.evalPowZeroInt

deleted def Mathlib.Meta.Positivity.evalRatCast

deleted def Mathlib.Meta.Positivity.evalZpow

Modified Mathlib/Tactic/Positivity/Core.lean

Modified Mathlib/Tactic/Rify.lean

Modified scripts/noshake.json

Modified test/norm_cast.lean