Commit 2020-09-25 19:15 85bbf8a5

feat(data/fin): zero_eq_one_iff and one_eq_zero_iff (#4255) Just a pair of little lemmas that were handy to me. The main benefit is that simp can now prove if (0 : fin 2) = 1 then 1 else 0 = 0, which should help with calculations using data.matrix.notation.