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.