Commit 2026-01-04 10:53 9bbace6f

View on Github →

feat(BigOperators/Finprod): add finsum_cond_pos (#33508)

Estimated changes

deleted theorem one_lt_finprod'
added theorem one_lt_finprod
added theorem one_lt_finprod_cond