Commit 2026-10-11 17:26 939d5d5d

View on Github →

chore: use the Finset.card notation more widely (#44638) Replace Finset.card s by #s in all files that do not mention other notions of cardinality. It would be nice to unify the notation for all notions, but this is left as further work. Generated by Claude Sonnet in a few prompts, reviewed line-by-line by myself. Assisted-by: Claude Sonnet 5.5

Estimated changes

modified theorem Cubic.card_roots_le
modified theorem Finset.card_smul_finset₀
modified theorem CovBy.card_finset
modified theorem Finset.grade_eq
modified theorem Finset.card_insertNone
modified theorem Option.card_toFinset
modified def PolynomialLaw.lifts
modified def PolynomialLaw.φ