Commit 2025-08-01 20:41 1e47c315
View on Github →feat(Algebra/BigOperators/Finprod): add powerset projection lemmas (#25965) This PR continues the work from #23926. Original PR: https://github.com/leanprover-community/mathlib4/pull/23926
feat(Algebra/BigOperators/Finprod): add powerset projection lemmas (#25965) This PR continues the work from #23926. Original PR: https://github.com/leanprover-community/mathlib4/pull/23926