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.

Estimated changes