no goals
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m✝ m : M
p : Polynomial { x // x ∈ subfield M F }
x : { x // x ∈ subfield M F }
⊢ m • ↑Polynomial.C x = ↑Polynomial.C x
rw [Polynomial.smul_C, smul]
no goals
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m✝ m : M
p✝ p q : Polynomial { x // x ∈ subfield M F }
ihp : m • p = p
ihq : m • q = q
⊢ m • (p + q) = p + q
rw [smul_add, ihp, ihq]
no goals
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m✝ m : M
p : Polynomial { x // x ∈ subfield M F }
n : ℕ
x : { x // x ∈ subfield M F }
x✝ : m • (↑Polynomial.C x * Polynomial.X ^ n) = ↑Polynomial.C x * Polynomial.X ^ n
⊢ m • (↑Polynomial.C x * Polynomial.X ^ (n + 1)) = ↑Polynomial.C x * Polynomial.X ^ (n + 1)
rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]