K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ ↑(algebraMap R (RatFunc K)) x = RatFunc.mk (↑(algebraMap R K[X]) x) 1
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ ↑(algebraMap R (RatFunc K)) x =
    ↑(algebraMap ((fun x => K[X]) x) (RatFunc K)) (↑(algebraMap R K[X]) x) / ↑(algebraMap K[X] (RatFunc K)) 1
rw [← mk_eq_div]
no goals
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ ↑(algebraMap R (RatFunc K)) x = RatFunc.mk (↑(algebraMap R K[X]) x) 1
rfl