R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (divX p) n = coeff p (1 + n)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (divX p) n = coeff p (n + 1)
rw [add_comm]
case ofFinsupp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (divX { toFinsupp := toFinsupp✝ }) n = coeff { toFinsupp := toFinsupp✝ } (1 + n)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (divX p) n = coeff p (1 + n)
cases p
no goals
case ofFinsupp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (divX { toFinsupp := toFinsupp✝ }) n = coeff { toFinsupp := toFinsupp✝ } (1 + n)
rfl