Commit 2024-01-04 01:46 570a85ce

View on Github →

chore: rename Finset.card_doubleton to Finset.card_pair (#9379)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Finset.card_doubleton

added theorem Finset.card_pair

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean