Commit 2023-07-24 07:51 ccbfd851

View on Github →

feat: missing lemma on finprod, modelled on the one on Finset.prod (#6070)

Estimated changes

added theorem one_lt_finprod'