R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ Finset.max {n} = ↑n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ degree (↑(monomial n) a) = ↑n
rw [degree, support_monomial n ha]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ Finset.max {n} = ↑n
rfl