Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 13:07 9a30f8cf

View on Github →

refactor(data/fin): drop fin.cast_add_right (#9371) This was a duplicate of fin.nat_add. Also simplify some definitions of equivalences.

Estimated changes

Modified src/data/equiv/fin.lean

added theorem fin_add_flip_apply_cast_add

deleted theorem fin_add_flip_apply_left

added theorem fin_add_flip_apply_mk_left

added theorem fin_add_flip_apply_mk_right

added theorem fin_add_flip_apply_nat_add

deleted theorem fin_add_flip_apply_right

added theorem fin_succ_equiv'_succ_above

added theorem fin_succ_equiv'_symm_some

modified theorem fin_sum_fin_equiv_symm_apply_cast_add

deleted theorem fin_sum_fin_equiv_symm_apply_cast_add_right

deleted theorem fin_sum_fin_equiv_symm_apply_left

added theorem fin_sum_fin_equiv_symm_apply_nat_add

deleted theorem fin_sum_fin_equiv_symm_apply_right

Modified src/data/fin.lean

modified def fin.add_cases

added theorem fin.add_nat_mk

added theorem fin.add_nat_sub_nat

added theorem fin.cast_add_cast_lt

added theorem fin.cast_add_nat

deleted def fin.cast_add_right

added theorem fin.cast_lt_cast_add

added theorem fin.cast_nat_add

deleted theorem fin.coe_cast_add_right

deleted theorem fin.le_cast_add_right

added theorem fin.le_coe_add_nat

added theorem fin.le_coe_nat_add

added theorem fin.nat_add_mk

added theorem fin.nat_add_sub_nat_cast

added theorem fin.sub_nat_add_nat

added theorem fin.sub_nat_mk