R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
this : Function.Injective fun c => c • 1
⊢ Function.Injective ↑(algebraMap R A)
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ Function.Injective ↑(algebraMap R A)
have := @smul_left_injective R A CommRing.toRing Ring.toAddCommGroup Algebra.toModule
  ‹_› 1 one_ne_zero
no goals
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
this : Function.Injective fun c => c • 1
⊢ Function.Injective ↑(algebraMap R A)
simpa only [algebraMap_eq_smul_one'] using this