Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 22:09 992354c2

View on Github →

feat(data/fintype): well_foundedness lemmas on fintypes (#1156)

feat(data/fintype): well_foundedness lemmas on fintypes
Update fintype.lean
minor fixes

Estimated changes

Modified src/data/fintype.lean

added theorem fintype.linear_order.is_well_order

added theorem fintype.preorder.well_founded

added theorem fintype.well_founded_of_trans_of_irrefl