Def Mathlib.Meta.Positivity.evalBoundingSieveWeights

Modification history

2025-05-25 13:18

Mathlib/NumberTheory/SelbergSieve.lean

chore(*): use `gcongr`&`positivity` (#25128)

Added Mathlib.Meta.Positivity.evalBoundingSieveWeights View on Github →