R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ ↑n = ↑n
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ trailingDegree (↑(monomial n) a) = ↑n
rw [trailingDegree, support_monomial n ha, min_singleton]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ ↑n = ↑n
rfl