Commit 2025-10-02 08:08 74c7a5cf

View on Github →

feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas (#27841)

Estimated changes

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

Modified Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem tprod_comp_neg

Modified Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

added theorem multipliable_pnat_iff_multipliable_succ

deleted theorem pnat_multipliable_iff_multipliable_succ

added theorem tprod_int_eq_zero_mul_tprod_pnat_sq

modified theorem tprod_pnat_eq_tprod_succ

added theorem tprod_zero_pnat_eq_tprod_nat