case ofFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
toFractionRing✝ : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
p : RatFunc K
⊢ (c • p).toFractionRing = c • p.toFractionRing
cases p
no goals
case ofFractionRing
K : Type u
inst✝¹ : CommRing K
R : Type u_1
inst✝ : SMul R (FractionRing K[X])
c : R
toFractionRing✝ : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing✝ }).toFractionRing = c • { toFractionRing := toFractionRing✝ }.toFractionRing
rw [← ofFractionRing_smul]