case intro
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : Monic P ∧ eval₂ (algebraMap R B) b P = 0
⊢ IsIntegral R (↑f b)
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ IsIntegral R (↑f b)
obtain ⟨P, hP⟩ := hb
case intro
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : Monic P ∧ eval₂ (algebraMap R B) b P = 0
⊢ eval₂ (algebraMap R ((fun x => C) b)) (↑f b) P = 0
case intro
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : Monic P ∧ eval₂ (algebraMap R B) b P = 0
⊢ IsIntegral R (↑f b)
refine' ⟨P, hP.1, _⟩
no goals
case intro
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : Monic P ∧ eval₂ (algebraMap R B) b P = 0
⊢ eval₂ (algebraMap R ((fun x => C) b)) (↑f b) P = 0
rw [← aeval_def, show (aeval (f b)) P = (aeval (f b)) (P.map (algebraMap R A)) by simp,
  aeval_algHom_apply, aeval_map_algebraMap, aeval_def, hP.2, _root_.map_zero]
no goals
R : Type u_4
A : Type u_5
B✝ : Type ?u.113227
S : Type ?u.113230
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B✝
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B✝
f✝ : R →+* S
B : Type u_1
C : Type u_2
F : Type u_3
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R C
inst✝³ : IsScalarTower R A B
inst✝² : Algebra A C
inst✝¹ : IsScalarTower R A C
b : B
inst✝ : AlgHomClass F A B C
f : F
P : R[X]
hP : Monic P ∧ eval₂ (algebraMap R B) b P = 0
⊢ ↑(aeval (↑f b)) P = ↑(aeval (↑f b)) (Polynomial.map (algebraMap R A) P)
simp