feat(algebra/char_zero): add a lemma ring_hom.injective_nat (#14414)

Note that there is a lemma `ring_hom.injective_int`.
leanprover-community · Jun 3, 2022 · 705160e · 705160e
1 parent d2dcb74
commit 705160e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/algebra/char_zero.lean b/src/algebra/char_zero.lean
@@ -225,4 +225,8 @@ lemma ring_hom.char_zero_iff {ϕ : R →+* S} (hϕ : function.injective ϕ) :
 ⟨λ hR, ⟨λ a b h, by rwa [←@nat.cast_inj R _ _ hR, ←hϕ.eq_iff, map_nat_cast ϕ, map_nat_cast ϕ]⟩,
   λ hS, by exactI ϕ.char_zero⟩
 
+lemma ring_hom.injective_nat (f : ℕ →+* R) [char_zero R] :
+  function.injective f :=
+subsingleton.elim (nat.cast_ring_hom _) f ▸ nat.cast_injective
+
 end ring_hom