diff --git a/Mathlib.lean b/Mathlib.lean
index 51a2d9e682d0ca..76ae6b4dedc9ff 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3820,6 +3820,7 @@ public import Mathlib.Data.FinEnum
 public import Mathlib.Data.FinEnum.Option
 public import Mathlib.Data.Finite.Card
 public import Mathlib.Data.Finite.Defs
+public import Mathlib.Data.Finite.Option
 public import Mathlib.Data.Finite.Perm
 public import Mathlib.Data.Finite.Prod
 public import Mathlib.Data.Finite.Set
diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean
new file mode 100644
index 00000000000000..6549e4a03b17d0
--- /dev/null
+++ b/Mathlib/Data/Finite/Option.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Alex Brodbelt. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Brodbelt, Eric Wieser
+-/
+module
+
+public import Mathlib.Data.Finite.Defs
+import Mathlib.Data.Fintype.Option
+import Mathlib.Logic.Equiv.Fin.Basic
+
+/-!
+# Finiteness conditions for `Option` types
+-/
+
+public section
+
+/-- The `Option` type on a type is finite if and only if the underlying type is finite. -/
+@[simp]
+theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where
+  mpr _ := inferInstance
+  mp
+  | @Finite.intro _ 0 e => (e none).elim0
+  | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩