case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R B) x p = 0
⊢ IsIntegral A x
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
h : IsIntegral R x
⊢ IsIntegral A x
rcases h with ⟨p, ⟨hp, hp'⟩⟩
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R B) x p = 0
⊢ IsIntegral A x
refine' ⟨p.map (algebraMap R A), ⟨hp.map (algebraMap R A), _⟩⟩
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
rw [IsScalarTower.algebraMap_eq R A B, ← eval₂_map] at hp'
no goals
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_2
S : Type ?u.1578175
T : Type ?u.1578178
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : B
p : R[X]
hp : Monic p
hp' : eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0
exact hp'