R✝ : Type u
S : Type ?u.101390
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 : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R (↑(algebraMap R A) ↑n)
R✝ : Type u
S : Type ?u.101390
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 : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n
rw [← map_ratCast (algebraMap R A)]
no goals
R✝ : Type u
S : Type ?u.101390
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 : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R (↑(algebraMap R A) ↑n)
exact isAlgebraic_algebraMap (Rat.cast n)