Commit 2025-12-24 11:27 8010f92a

View on Github →

chore: reduce reliance on Nat.card definition (#33245) The new proofs don't rely on Nat.card being defined in terms of cardinals, and are cleaner anyway.

Estimated changes