PR !4#17499: feat: more lemmas about `Fin`-indexed produc...

Stream: triage

[Random Issue Bot]

Today I chose PR 17499 for discussion!

feat: more lemmas about Fin-indexed products of finsets
Created by @Yaël Dillies (@YaelDillies) on 2024-10-07
Labels: t-data

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Awaiting review. Last missing piece before we get Schwartz-Zippel in mathlib!