R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : degree f = ⊥
⊢ f = 0
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ degree f = ⊥ ↔ f = 0
refine' ⟨fun h => _, fun h => by rw [h, degree_zero]⟩
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
⊢ f = 0
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : degree f = ⊥
⊢ f = 0
rw [degree, Finset.max_eq_sup_withBot] at h
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
⊢ ↑f n = ↑0 n
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
⊢ f = 0
ext n
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
f0 : ¬↑f n = ↑0 n
⊢ False
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
⊢ ↑f n = ↑0 n
refine' not_not.mp fun f0 => _
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
f0 : ¬↑f n = ↑0 n
h : ∀ (s : ℤ), ¬↑f s = 0 → False
⊢ False
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
f0 : ¬↑f n = ↑0 n
⊢ False
simp_rw [Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne.def, WithBot.coe_ne_bot] at h
no goals
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
f0 : ¬↑f n = ↑0 n
h : ∀ (s : ℤ), ¬↑f s = 0 → False
⊢ False
exact h n f0
no goals
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ degree f = ⊥
rw [h, degree_zero]