Commit 2023-09-14 12:44 b2dbb2c6

View on Github →

feat(UniqueProds): subsingleton and MulOpposite lemmas (#6755) Basic support for subsingleton and MulOpposites. Helps #6723.

Estimated changes

Modified Mathlib/Algebra/Group/UniqueProds.lean

added theorem UniqueMul.iff_mulOpposite

added theorem UniqueMul.of_mulOpposite

added theorem UniqueMul.of_subsingleton

added theorem UniqueMul.to_mulOpposite

added theorem UniqueProds.iff_mulOpposite

added theorem UniqueProds.of_mulOpposite

added theorem UniqueProds.of_subsingleton