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
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
rw [← CharP.cast_eq_zero_iff R p x]
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
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
change algebraMap ℕ A x = 0 ↔ algebraMap ℕ R x = 0
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
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
rw [IsScalarTower.algebraMap_apply ℕ R A x]
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
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
refine' Iff.trans _ h.eq_iff
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)
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = 0 ↔ ↑(algebraMap R A) (↑(algebraMap ℕ R) x) = ↑(algebraMap R A) 0
rw [RingHom.map_zero]