mathlib

31cb3c16 - chore(algebra/group_with_zero/basic): generalize `units.exists_iff_ne_zero` to arbitrary propositions (#12439)

chore(algebra/group_with_zero/basic): generalize `units.exists_iff_ne_zero` to arbitrary propositions (#12439) This adds a more powerful version of this lemma that allows an existential to be replaced with one over the underlying group with zero. The naming matches `subtype.exists` and `subtype.exists'`, while the trailing zero matches `units.mk0`.