R : Type u_1
A : Type ?u.981430
B : Type ?u.981433
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f : R →+* S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (leadingCoeff p • x)
R : Type u_1
A : Type ?u.981430
B : Type ?u.981433
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f : R →+* S
p : R[X]
x : S
inst✝ : Algebra R S
h : ↑(aeval x) p = 0
⊢ IsIntegral R (leadingCoeff p • x)
rw [aeval_def] at h
R : Type u_1
A : Type ?u.981430
B : Type ?u.981433
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f : R →+* S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (↑(algebraMap R S) (leadingCoeff p) * x)
R : Type u_1
A : Type ?u.981430
B : Type ?u.981433
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f : R →+* S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (leadingCoeff p • x)
rw [Algebra.smul_def]
no goals
R : Type u_1
A : Type ?u.981430
B : Type ?u.981433
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f : R →+* S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (↑(algebraMap R S) (leadingCoeff p) * x)
exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h