Mathlib Changelog
v3
Changelog
About
Github
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