Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 14:28 c7aa2dfa

View on Github →

refactor(data/fin/basic): merge fin.rev and order_iso.fin_equiv (#16745) Also add some missing lemmas.

Estimated changes

added theorem fin.coe_rev
modified theorem fin.is_lt
added theorem fin.last_sub
modified theorem fin.pos_iff_nonempty
modified def fin.rev
added theorem fin.rev_bijective
added theorem fin.rev_inj
added theorem fin.rev_injective
added theorem fin.rev_involutive
added theorem fin.rev_le_rev
added theorem fin.rev_lt_rev
added theorem fin.rev_rev
added theorem fin.rev_surjective
added theorem fin.rev_symm
modified theorem fin.sub_one_lt_iff
deleted def order_iso.fin_equiv
deleted theorem order_iso.fin_equiv_apply