Commit 2026-01-05 17:02 05f342bf

View on Github →

chore(positivity): make tactic lemmas public (#33593) This PR removes privateInPublic and private from all lemmas used by the positivity tactic. These lemmas are part of the public API of the positivity tactic, so it makes sense for the lemmas to be public. They all live in the Mathlib.Meta.Positivity namespace, so they can't be confused with user-facing lemmas.

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

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

added theorem Mathlib.Meta.Positivity.div_ne_zero_of_ne_zero_of_pos

added theorem Mathlib.Meta.Positivity.div_ne_zero_of_pos_of_ne_zero

added theorem Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos

added theorem Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg

added theorem Mathlib.Meta.Positivity.zpow_zero_pos

Modified Mathlib/Algebra/Order/Floor/Extended.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

added theorem Mathlib.Meta.Positivity.int_ceil_pos

added theorem Mathlib.Meta.Positivity.int_floor_nonneg

added theorem Mathlib.Meta.Positivity.int_floor_nonneg_of_pos

added theorem Mathlib.Meta.Positivity.nat_ceil_pos

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

added theorem Mathlib.Meta.Positivity.smul_ne_zero_of_ne_zero_of_pos

added theorem Mathlib.Meta.Positivity.smul_ne_zero_of_pos_of_ne_zero

added theorem Mathlib.Meta.Positivity.smul_nonneg_of_nonneg_of_pos

added theorem Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg

added theorem Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_pos

Modified Mathlib/Analysis/Complex/Order.lean

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

Modified Mathlib/Data/NNReal/Defs.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

added theorem Mathlib.Meta.Positivity.abs_pos_of_ne_zero

added theorem Mathlib.Meta.Positivity.int_div_nonneg_of_nonneg_of_pos

added theorem Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_nonneg

added theorem Mathlib.Meta.Positivity.int_div_nonneg_of_pos_of_pos

added theorem Mathlib.Meta.Positivity.int_div_self_pos

added theorem Mathlib.Meta.Positivity.int_natAbs_pos

added theorem Mathlib.Meta.Positivity.ite_ne_zero

added theorem Mathlib.Meta.Positivity.ite_ne_zero_of_ne_zero_of_pos

added theorem Mathlib.Meta.Positivity.ite_ne_zero_of_pos_of_ne_zero

added theorem Mathlib.Meta.Positivity.ite_nonneg

added theorem Mathlib.Meta.Positivity.ite_nonneg_of_nonneg_of_pos

added theorem Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg

added theorem Mathlib.Meta.Positivity.ite_pos

added theorem Mathlib.Meta.Positivity.le_min_of_le_of_lt

added theorem Mathlib.Meta.Positivity.le_min_of_lt_of_le

added theorem Mathlib.Meta.Positivity.max_ne

added theorem Mathlib.Meta.Positivity.min_ne

added theorem Mathlib.Meta.Positivity.min_ne_of_lt_of_ne

added theorem Mathlib.Meta.Positivity.min_ne_of_ne_of_lt

added theorem Mathlib.Meta.Positivity.pow_zero_pos

Modified Mathlib/Tactic/Positivity/Core.lean