feat: add Commute.of_map (#5316)

elements commute if their images under and injective `MulHom` do.
leanprover-community · Jun 20, 2023 · 712f6d7 · 712f6d7
1 parent c511043
commit 712f6d7
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Hom/Commute.lean b/Mathlib/Algebra/Hom/Commute.lean
@@ -34,4 +34,14 @@ protected theorem Commute.map [MulHomClass F M N] (h : Commute x y) (f : F) : Co
 #align commute.map Commute.map
 #align add_commute.map AddCommute.map
 
+@[to_additive (attr := simp)]
+protected theorem SemiconjBy.of_map [MulHomClass F M N] (f : F) (hf : Function.Injective f)
+    (h : SemiconjBy (f a) (f x) (f y)) : SemiconjBy a x y :=
+  hf (by simpa only [SemiconjBy, map_mul] using h)
+
+@[to_additive (attr := simp)]
+theorem Commute.of_map [MulHomClass F M N] {f : F} (hf : Function.Injective f)
+    (h : Commute (f x) (f y)) : Commute x y :=
+  hf (by simpa only [map_mul] using h.eq)
+
 end Commute