Commit 2023-06-22 09:57 8c343e58

View on Github →

chore: forward-port mathlib#19204 (#5369)

Estimated changes

Modified Mathlib/Algebra/Invertible.lean

added def Invertible.copy'

added def Invertible.mul

added def Invertible.mulLeft

added def Invertible.mulRight

added def invertibleOfInvertibleMul

added def invertibleOfMulInvertible