Commit 2025-07-04 14:26 fe095645

View on Github →

chore(Finset/Card): cleanup section and improve documentation (#26373)

Use the Set.MapsTo spelling (and similar) where possible, for consistency throughout mathlib
Improve documentation on some lemmas ("reorder" has little meaning on finsets, which are inherently unordered)
Add documentation to other lemmas

Estimated changes

Modified Archive/Imo/Imo2024Q3.lean

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_le_card_of_injOn

modified theorem Finset.card_nbij'

modified theorem Finset.card_nbij

modified theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to

added theorem Set.BijOn.finsetCard_eq

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/Setoid/Partition/Card.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/MaricaSchoenheim.lean

Modified Mathlib/RingTheory/IntegralDomain.lean