case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.210572
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f✝ : R →+* S
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : Monic f
hx : eval₂ (_root_.algebraMap R A) x f = 0
⊢ IsIntegral R (↑(_root_.algebraMap A B) x)
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.210572
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f : R →+* S
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
h : IsIntegral R x
⊢ IsIntegral R (↑(_root_.algebraMap A B) x)
rcases h with ⟨f, hf, hx⟩
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.210572
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f✝ : R →+* S
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : Monic f
hx : eval₂ (_root_.algebraMap R A) x f = 0
⊢ eval₂ (_root_.algebraMap R ((fun x => B) x)) (↑(_root_.algebraMap A B) x) f = 0
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.210572
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f✝ : R →+* S
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : Monic f
hx : eval₂ (_root_.algebraMap R A) x f = 0
⊢ IsIntegral R (↑(_root_.algebraMap A B) x)
use f, hf
no goals
case intro.intro
R : Type u_3
A : Type u_1
B : Type u_2
S : Type ?u.210572
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f✝ : R →+* S
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : Monic f
hx : eval₂ (_root_.algebraMap R A) x f = 0
⊢ eval₂ (_root_.algebraMap R ((fun x => B) x)) (↑(_root_.algebraMap A B) x) f = 0
rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, RingHom.map_zero]