mathlib
340178d8 - feat(data/finset): inj_on_of_surj_on_of_card_le (#1578)

Commit

6 years ago

feat(data/finset): inj_on_of_surj_on_of_card_le (#1578) * feat(data/finset): inj_on_of_surj_on_of_card_le * Type ascriptions * function namespace

References

Author

ChrisHughes24

Committer

mergify[bot]

Parents