R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
x✝¹ : R
x✝ : A
⊢ ↑(algebraMap A B) (x✝¹ • x✝) = x✝¹ • ↑(algebraMap A B) x✝
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
⊢ NoZeroSMulDivisors R A
refine'
  Function.Injective.noZeroSMulDivisors _ (IsIntegralClosure.algebraMap_injective A R B)
    (map_zero _) fun _ _ => _
no goals
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
x✝¹ : R
x✝ : A
⊢ ↑(algebraMap A B) (x✝¹ • x✝) = x✝¹ • ↑(algebraMap A B) x✝
simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]