Commit 2025-01-13 10:02 cf581dca

View on Github →

feat: (∏ᶠ i, f i) a = ∏ᶠ i, f i a (#20203) From FLT

Estimated changes

added theorem finprod_apply
added theorem finprod_apply_ne_one
modified theorem finprod_mem_mulSupport
added theorem finprod_option