R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap ℕ A) x = ↑(algebraMap ℕ A) y
⊢ x = y
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑x = ↑y
⊢ x = y
change algebraMap ℕ A x = algebraMap ℕ A y at hxy
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap ℕ A) y
⊢ x = y
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap ℕ A) x = ↑(algebraMap ℕ A) y
⊢ x = y
rw [IsScalarTower.algebraMap_apply ℕ R A x] at hxy
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) (↑(algebraMap ℕ R) y)
⊢ x = y
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap ℕ A) y
⊢ x = y
rw [IsScalarTower.algebraMap_apply ℕ R A y] at hxy
no goals
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
inst✝ : CharZero R
x y : ℕ
hxy : ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) (↑(algebraMap ℕ R) y)
⊢ x = y
exact CharZero.cast_injective (h hxy)