From e0dd30031013653bccdac0a4fa58e413453e4678 Mon Sep 17 00:00:00 2001 From: damiano Date: Sat, 7 May 2022 20:15:08 +0000 Subject: [PATCH] =?UTF-8?q?feat(algebra/{invertible=20+=20group=5Fpower/le?= =?UTF-8?q?mmas}):=20taking=20`inv=5Fof`=20(=E2=85=9F=5F)=20is=20injective?= =?UTF-8?q?=20(#14011)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Besides the lemma stated in the description, I also made explicit an argument that was implicit in a different lemma and swapped the arguments of `invertible_unique` in order to get the typeclass assumptions before some non-typeclass assumptions. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/inv_of_inj) Co-authored-by: Floris van Doorn <[fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)> --- src/algebra/group_power/lemmas.lean | 2 +- src/algebra/invertible.lean | 10 +++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean index 2410fcf2a94bc..56a4139af2701 100644 --- a/src/algebra/group_power/lemmas.lean +++ b/src/algebra/group_power/lemmas.lean @@ -41,7 +41,7 @@ instance invertible_pow (m : M) [invertible m] (n : ℕ) : invertible (m ^ n) := lemma inv_of_pow (m : M) [invertible m] (n : ℕ) [invertible (m ^ n)] : ⅟(m ^ n) = ⅟m ^ n := -@invertible_unique M _ (m ^ n) (m ^ n) rfl ‹_› (invertible_pow m n) +@invertible_unique M _ (m ^ n) (m ^ n) _ (invertible_pow m n) rfl lemma is_unit.pow {m : M} (n : ℕ) : is_unit m → is_unit (m ^ n) := λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩ diff --git a/src/algebra/invertible.lean b/src/algebra/invertible.lean index 19ebbb9f01ec6..f1ab5c27eaf50 100644 --- a/src/algebra/invertible.lean +++ b/src/algebra/invertible.lean @@ -97,8 +97,8 @@ left_inv_eq_right_inv (inv_of_mul_self _) hac lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] (hac : b * a = 1) : ⅟a = b := (left_inv_eq_right_inv hac (mul_inv_of_self _)).symm -lemma invertible_unique {α : Type u} [monoid α] (a b : α) (h : a = b) - [invertible a] [invertible b] : +lemma invertible_unique {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] + (h : a = b) : ⅟a = ⅟b := by { apply inv_of_eq_right_inv, rw [h, mul_inv_of_self], } @@ -177,10 +177,14 @@ by simp only [←two_mul, mul_inv_of_self] instance invertible_inv_of [has_one α] [has_mul α] {a : α} [invertible a] : invertible (⅟a) := ⟨ a, mul_inv_of_self a, inv_of_mul_self a ⟩ -@[simp] lemma inv_of_inv_of [monoid α] {a : α} [invertible a] [invertible (⅟a)] : +@[simp] lemma inv_of_inv_of [monoid α] (a : α) [invertible a] [invertible (⅟a)] : ⅟(⅟a) = a := inv_of_eq_right_inv (inv_of_mul_self _) +@[simp] lemma inv_of_inj [monoid α] {a b : α} [invertible a] [invertible b] : + ⅟ a = ⅟ b ↔ a = b := +⟨invertible_unique _ _, invertible_unique _ _⟩ + /-- `⅟b * ⅟a` is the inverse of `a * b` -/ def invertible_mul [monoid α] (a b : α) [invertible a] [invertible b] : invertible (a * b) := ⟨ ⅟b * ⅟a, by simp [←mul_assoc], by simp [←mul_assoc] ⟩