Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-14 10:51 ba9d551a

View on Github →

chore(algebra/invertible): minor golf (#14141)

Estimated changes

Modified src/algebra/invertible.lean

modified theorem inv_of_inv_of

modified theorem inv_of_mul

modified theorem nonempty_invertible_iff_is_unit