Commit 2024-02-08 10:24 4656d545

View on Github →

chore: remove unnecessary Mathlib.Meta.Positivity namespacing (#10343)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

modified def Mathlib.Meta.Positivity.evalRpow

modified def Mathlib.Meta.Positivity.evalRpowZero

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

modified def Mathlib.Meta.Positivity.evalRealPi

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

added def Mathlib.Meta.Positivity.evalBound

added def Mathlib.Meta.Positivity.evalInitialBound

deleted def Tactic.evalBound

deleted def Tactic.evalInitialBound