Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 15:56 11e1cc36

View on Github →

feat(data/equiv/basic): Add fin_succ_above_equiv (#5145)

Estimated changes

Modified src/data/equiv/fin.lean

added def fin_succ_equiv'

added theorem fin_succ_equiv'_above

added theorem fin_succ_equiv'_at

added theorem fin_succ_equiv'_below

added theorem fin_succ_equiv'_symm_none

added theorem fin_succ_equiv'_zero

modified def fin_succ_equiv

added theorem fin_succ_equiv_symm'_coe_above

added theorem fin_succ_equiv_symm'_coe_below

added theorem fin_succ_equiv_symm'_some_above

added theorem fin_succ_equiv_symm'_some_below

added theorem fin_succ_equiv_symm_coe

Modified src/data/fin.lean

modified theorem fin.cast_succ_pos

added theorem fin.pred_above_above

added theorem fin.pred_above_below

added theorem fin.pred_above_last

added theorem fin.pred_above_last_apply

added theorem fin.pred_cast_succ_succ

Modified src/data/mv_polynomial/equiv.lean

Modified src/linear_algebra/linear_independent.lean