case ofFractionRing
K : Type u
inst✝ : CommRing K
R : Type ?u.178730
r : K
x : FractionRing K[X]
⊢ r • { toFractionRing := x } = ↑Polynomial.C r • { toFractionRing := x }
K : Type u
inst✝ : CommRing K
R : Type ?u.178730
x : RatFunc K
r : K
⊢ r • x = ↑Polynomial.C r • x
cases' x with x
case ofFractionRing.H
K : Type u
inst✝ : CommRing K
R : Type ?u.178730
r : K
y✝ : K[X] × { x // x ∈ K[X]⁰ }
⊢ r • { toFractionRing := Localization.mk y✝.fst y✝.snd } =
    ↑Polynomial.C r • { toFractionRing := Localization.mk y✝.fst y✝.snd }
case ofFractionRing
K : Type u
inst✝ : CommRing K
R : Type ?u.178730
r : K
x : FractionRing K[X]
⊢ r • { toFractionRing := x } = ↑Polynomial.C r • { toFractionRing := x }
induction x using Localization.induction_on
no goals
case ofFractionRing.H
K : Type u
inst✝ : CommRing K
R : Type ?u.178730
r : K
y✝ : K[X] × { x // x ∈ K[X]⁰ }
⊢ r • { toFractionRing := Localization.mk y✝.fst y✝.snd } =
    ↑Polynomial.C r • { toFractionRing := Localization.mk y✝.fst y✝.snd }
rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
  Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]