Commit 2025-10-04 03:18 9358199a

View on Github →

chore(Data/Finite): deprecate card_le_of_injective, card_le_of_surjective and card_sum (#28492)

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Modified Mathlib/Data/Finite/Card.lean

deleted theorem Finite.card_le_of_injective

deleted theorem Finite.card_le_of_surjective

deleted theorem Finite.card_sum

Modified Mathlib/GroupTheory/CommutingProbability.lean

Modified Mathlib/GroupTheory/Index.lean