Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-11 15:23 0bd2ea37

View on Github →

refactor(data/fin/basic): fin refactor to use ne_zero (#18107)

Estimated changes

modified theorem fin.bot_eq_zero
modified theorem fin.cast_succ_eq_zero_iff
modified theorem fin.cast_succ_ne_zero_iff
modified theorem fin.cast_succ_pos
modified theorem fin.cast_succ_zero
modified theorem fin.cast_zero
modified theorem fin.coe_bit1
modified theorem fin.coe_coe_eq_self
modified theorem fin.coe_coe_of_lt
modified theorem fin.coe_one'
modified theorem fin.coe_one
modified theorem fin.coe_val_eq_self
modified theorem fin.coe_val_of_lt
modified theorem fin.coe_zero
modified theorem fin.le_zero_iff
modified theorem fin.mk_bit1
modified theorem fin.mk_zero
added theorem fin.of_nat'_eq_coe
modified theorem fin.one_eq_zero_iff
modified theorem fin.pos_iff_ne_zero
modified theorem fin.succ_above_eq_zero_iff
modified theorem fin.succ_above_ne_zero
modified theorem fin.succ_above_ne_zero_zero
modified theorem fin.succ_above_pos
added theorem fin.succ_one_eq_two'
modified theorem fin.succ_one_eq_two
modified theorem fin.succ_succ_above_one
modified theorem fin.succ_succ_above_zero
added theorem fin.succ_zero_eq_one'
modified theorem fin.succ_zero_eq_one
modified theorem fin.val_one
modified theorem fin.val_zero'
modified theorem fin.zero_eq_one_iff
modified theorem fin.zero_le