Commit 2022-03-04 15:24 31cb3c16

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.