R : Type u_3
A : Type u_2
B : Type ?u.660893
S : Type u_1
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 S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
x : A
r : R
hx : IsIntegral S x
⊢ IsIntegral S (↑(algebraMap S A) (↑(algebraMap R S) r) * x)
R : Type u_3
A : Type u_2
B : Type ?u.660893
S : Type u_1
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 S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
x : A
r : R
hx : IsIntegral S x
⊢ IsIntegral S (r • x)
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S A]
no goals
R : Type u_3
A : Type u_2
B : Type ?u.660893
S : Type u_1
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 S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
x : A
r : R
hx : IsIntegral S x
⊢ IsIntegral S (↑(algebraMap S A) (↑(algebraMap R S) r) * x)
exact isIntegral_mul isIntegral_algebraMap hx