Commit 2023-01-23 12:02 c40a401e

View on Github →

feat: port Algebra.Group.UniqueProds (#1764)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/UniqueProds.lean

added theorem UniqueMul.exists_iff_exists_existsUnique

added theorem UniqueMul.iff_existsUnique

added theorem UniqueMul.mt

added theorem UniqueMul.mulHom_image_iff

added theorem UniqueMul.mulHom_map_iff

added theorem UniqueMul.mulHom_preimage

added theorem UniqueMul.set_subsingleton

added theorem UniqueMul.subsingleton

added def UniqueMul

added theorem eq_and_eq_of_le_of_le_of_mul_le