Theorem: isEmpty_fin_iff (Matroid/ForMathlib/Other.lean)

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
m n R : Type
inst✝ : Semiring R
b : ℕ
⊢ IsEmpty (Fin b) ↔ b = 0
Tactic:
cases b <;> simp [Fin.isEmpty]
State after:
no goals