Theorem: algebraMap_injective' (DividedPowers/ForMathlib/AlgebraComp.lean)

State before:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑(algebraMap R K)
Tactic:
rw [IsScalarTower.algebraMap_eq R A K]
State after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑((algebraMap A K).comp (algebraMap R A))

State before:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑((algebraMap A K).comp (algebraMap R A))
Tactic:
apply Function.Injective.comp (RingHom.injective (algebraMap A K)) (IsFractionRing.injective R A)
State after:
no goals