feat(data/equiv/*): to_monoid_hom_injective and to_ring_hom_injective (…

…#4525)
leanprover-community · Oct 8, 2020 · 60be8ed · 60be8ed
1 parent 253f225
commit 60be8ed
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean
@@ -222,6 +222,10 @@ begin
   { exact congr_arg equiv.inv_fun h₁ }
 end
 
+@[to_additive] lemma to_monoid_hom_injective
+  {M N} [monoid M] [monoid N] : function.injective (to_monoid_hom : (M ≃* N) → M →* N) :=
+λ f g h, mul_equiv.ext (monoid_hom.ext_iff.1 h)
+
 attribute [ext] add_equiv.ext
 
 end mul_equiv

diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
@@ -190,6 +190,9 @@ variables [semiring R] [semiring S] [semiring S']
 def to_ring_hom (e : R ≃+* S) : R →+* S :=
 { .. e.to_mul_equiv.to_monoid_hom, .. e.to_add_equiv.to_add_monoid_hom }
 
+lemma to_ring_hom_injective : function.injective (to_ring_hom : (R ≃+* S) → R →+* S) :=
+λ f g h, ring_equiv.ext (ring_hom.ext_iff.1 h)
+
 instance has_coe_to_ring_hom : has_coe (R ≃+* S) (R →+* S) := ⟨ring_equiv.to_ring_hom⟩
 
 @[norm_cast] lemma coe_ring_hom (f : R ≃+* S) (a : R) :