[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R p x]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ ↑x = 0
[PROOFSTEP]
change algebraMap ℕ A x = 0 ↔ algebraMap ℕ R x = 0
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap ℕ A) x = 0 ↔ ↑(algebraMap ℕ R) x = 0
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A x]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = 0 ↔ ↑(algebraMap ℕ R) x = 0
[PROOFSTEP]
refine' Iff.trans _ h.eq_iff
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
h : Function.Injective ↑(algebraMap R A)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = 0 ↔ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) 0
[PROOFSTEP]
rw [RingHom.map_zero]
[GOAL]
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
[PROOFSTEP]
change algebraMap ℕ A x = algebraMap ℕ A y at hxy 
[GOAL]
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
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A x] at hxy 
[GOAL]
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
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply ℕ R A y] at hxy 
[GOAL]
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
[PROOFSTEP]
exact CharZero.cast_injective (h hxy)
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ ringChar K = ringChar L
[PROOFSTEP]
rw [ringChar.eq_iff, Algebra.charP_iff K L]
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)
[PROOFSTEP]
apply ringChar.charP
