Commit 2025-03-01 16:22 7f82eb86

View on Github →

feat(Data/Fin): add @[simp] lemmas (#22259)

Estimated changes

deleted theorem Fin.castSucc_pos'
added theorem Fin.castSucc_pos_iff
added theorem Fin.mk_eq_one
added theorem Fin.mk_eq_zero
added theorem Fin.one_eq_mk
added theorem Fin.val_eq_zero_iff
added theorem Fin.val_ne_zero_iff
added theorem Fin.val_pos_iff
deleted theorem Fin.val_zero'
added theorem Fin.zero_eq_mk