feat(data/fin): `zero_eq_one_iff` and `one_eq_zero_iff` (#4255)
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`.






leanprover-community/mathlib,leanprover-community/mathlib