Theorem Finite.card_le_of_surjective

Modification history

2025-10-04 03:18

Mathlib/Data/Finite/Card.lean

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

Deleted Finite.card_le_of_surjective View on Github →

2023-02-11 15:47

Mathlib/Data/Finite/Card.lean

feat: Port Data.Finite.Card (#2183)

Added Finite.card_le_of_surjective View on Github →