Theorem UniqueMul.exists_iff_exists_existsUnique

Modification history

2023-01-23 12:02
Mathlib/Algebra/Group/UniqueProds.lean
feat: port Algebra.Group.UniqueProds (#1764)
Added UniqueMul.exists_iff_exists_existsUniqueView on Github →