Commit 2025-03-04 17:12 d0f85ee2
View on Github →feat: product using Function.extend (#22551)
Given s : Finset α and f : s → β we have ∏ x, f x = ∏ x ∈ s, Subtype.val.extend f 1 x.
Specialize Function.extend_apply to the case where f = Subtype.val.