Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information