From d301d431feb4c68cf7f3a0993018a706c01e9b9c Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 29 Sep 2020 12:11:45 +0000 Subject: [PATCH] feat(algebra/invertible): invertible.copy (#4318) A useful gadget from the Witt vector project. Co-authored by: Johan Commelin Co-authored-by: Rob Lewis --- src/algebra/invertible.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/algebra/invertible.lean b/src/algebra/invertible.lean index 9d78a1351b387..a72964b00257f 100644 --- a/src/algebra/invertible.lean +++ b/src/algebra/invertible.lean @@ -134,6 +134,15 @@ lemma inv_of_mul [monoid α] (a b : α) [invertible a] [invertible b] [invertibl ⅟(a * b) = ⅟b * ⅟a := inv_of_eq_right_inv (by simp [←mul_assoc]) +/-- +If `r` is invertible and `s = r`, then `s` is invertible. +-/ +def invertible.copy [monoid α] {r : α} (hr : invertible r) (s : α) (hs : s = r) : invertible s := +{ inv_of := ⅟r, + inv_of_mul_self := by rw [hs, inv_of_mul_self], + mul_inv_of_self := by rw [hs, mul_inv_of_self] } + + lemma commute_inv_of {M : Type*} [has_one M] [has_mul M] (m : M) [invertible m] : commute m (⅟m) := calc m * ⅟m = 1 : mul_inv_of_self m