case intro.intro
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ IsAlgebraic R r
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
⊢ IsAlgebraic R r
obtain ⟨p, p_nonzero, hp⟩ := ht
case intro.intro.refine_1
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(expand R n) p ≠ 0

case intro.intro.refine_2
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(aeval r) (↑(expand R n) p) = 0
case intro.intro
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ IsAlgebraic R r
refine ⟨Polynomial.expand _ n p, ?_, ?_⟩
no goals
case intro.intro.refine_1
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(expand R n) p ≠ 0
rwa [Polynomial.expand_ne_zero hn]
no goals
case intro.intro.refine_2
R : Type u
S : Type ?u.226844
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : A
n : ℕ
hn : 0 < n
p : R[X]
p_nonzero : p ≠ 0
hp : ↑(aeval (r ^ n)) p = 0
⊢ ↑(aeval r) (↑(expand R n) p) = 0
rwa [Polynomial.expand_aeval n p r]