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
.