Commit 2022-12-07 15:23 811a6276

View on Github →

port: Algebra.Hom.Equiv.Units.Basic and Algebra.Order.Group.OrderIso (#895) a95b16cbade0f938fc24abd05412bde1e84bab9b

Estimated changes

added theorem Equiv.coe_mulLeft
added theorem Equiv.coe_mulRight
added theorem Equiv.mulLeft_symm
added theorem Equiv.mulRight_symm
added def MulEquiv.inv
added theorem MulEquiv.inv_symm
added theorem Units.coe_mapEquiv
added def Units.mapEquiv
added theorem Units.mapEquiv_symm
added def Units.mulLeft
added theorem Units.mulLeft_symm
added def Units.mulRight
added theorem Units.mulRight_symm
added theorem coe_toUnits
added def toUnits
added def OrderIso.inv
added def OrderIso.mulLeft
added theorem OrderIso.mulLeft_symm
added theorem OrderIso.mulRight_symm
added theorem inv_le'
added theorem le_inv'