Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 13:50 72308d85

View on Github →

chore(data/fin): use uniform names; restructure

Estimated changes

Modified data/equiv/fin.lean

added def fin_one_equiv

added def fin_two_equiv

added def fin_zero_equiv

Modified data/fin.lean

modified def fin.add_nat

added theorem fin.add_nat_val

deleted def fin.ascend

deleted theorem fin.ascend_descend

deleted theorem fin.ascend_ne

modified def fin.cases

modified theorem fin.cases_succ

modified theorem fin.cases_zero

added def fin.cast

added def fin.cast_le

added def fin.cast_lt

added theorem fin.cast_lt_val

added def fin.cast_succ

added theorem fin.cast_succ_cast_lt

added theorem fin.cast_succ_val

deleted def fin.descend

deleted theorem fin.descend_ascend

deleted theorem fin.eq_of_lt_succ_of_not_lt

deleted theorem fin.fin.raise_val

deleted def fin.fin_zero_elim

added theorem fin.le_iff_val_le_val

deleted def fin.lower

deleted def fin.lower_left

deleted def fin.lower_right

deleted theorem fin.lower_val

added theorem fin.lt_iff_val_lt_val

deleted def fin.nat_add

added def fin.pred_above

added theorem fin.pred_above_succ_above

deleted def fin.raise

deleted theorem fin.raise_lower

deleted def fin.raise_nat

deleted theorem fin.raise_val

added def fin.sub_nat

added theorem fin.sub_nat_val

added def fin.succ_above

added theorem fin.succ_above_descend

added theorem fin.succ_above_ne

modified theorem fin.succ_rec_on_succ

modified theorem fin.succ_rec_on_zero

added theorem fin.zero_le

added def fin_zero_elim

Modified data/nat/basic.lean

added theorem nat.eq_of_lt_succ_of_not_lt