K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (ofFractionRing ∘ ↑(algebraMap K[X] (FractionRing K[X])))
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ↑(algebraMap K[X] (RatFunc K))
rw [← ofFractionRing_comp_algebraMap]
no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (ofFractionRing ∘ ↑(algebraMap K[X] (FractionRing K[X])))
exact ofFractionRing_injective.comp (IsFractionRing.injective _ _)