case intro.intro
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type ?u.661802
n : ℕ
a : R
h : card (support (↑(monomial n) a)) ≤ 1
⊢ ↑(monomial (natDegree (↑(monomial n) a))) (leadingCoeff (↑(monomial n) a)) = ↑(monomial n) a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.661802
h : card (support p) ≤ 1
⊢ ↑(monomial (natDegree p)) (leadingCoeff p) = p
rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
no goals
case intro.intro
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
q : R[X]
ι : Type ?u.661802
n : ℕ
a : R
h : card (support (↑(monomial n) a)) ≤ 1
⊢ ↑(monomial (natDegree (↑(monomial n) a))) (leadingCoeff (↑(monomial n) a)) = ↑(monomial n) a
by_cases ha : a = 0 <;> simp [ha]