Commit 2025-09-15 18:23 3a0fa9d1

View on Github →

feat(ArithmeticFunction): lemmas about positivity (#28789) Add lemmas like σ k n = 0 ↔ n = 0. Also add positivity extensions for zeta and sigma.

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.cardDistinctFactors_eq_zero

added theorem ArithmeticFunction.cardDistinctFactors_pos

added theorem ArithmeticFunction.sigma_eq_zero

added theorem ArithmeticFunction.sigma_pos_iff

added theorem ArithmeticFunction.zeta_eq_zero

added theorem ArithmeticFunction.zeta_pos

added def Mathlib.Meta.Positivity.evalArithmeticFunctionSigma

added def Mathlib.Meta.Positivity.evalArithmeticFunctionZeta

Modified MathlibTest/positivity.lean