Commit 2023-03-01 18:09 26b92df7

View on Github →

chore: fix naming of Finset.pi.cons (#2553) This renames Finset.pi.cons to Finset.Pi.cons to match Multiset.Pi.cons. This doesn't need a backport, as it was just a mistake in the initial port in #1590.

Estimated changes