diff --git a/Mathlib.lean b/Mathlib.lean
index 51a2d9e682d0ca..3aceeeee73aeeb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3820,11 +3820,14 @@ 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
 public import Mathlib.Data.Finite.Sigma
+public import Mathlib.Data.Finite.Subtype
 public import Mathlib.Data.Finite.Sum
+public import Mathlib.Data.Finite.Units
 public import Mathlib.Data.Finite.Vector
 public import Mathlib.Data.Finmap
 public import Mathlib.Data.Finset.Attach
diff --git a/Mathlib/Data/Finite/Option.lean b/Mathlib/Data/Finite/Option.lean
new file mode 100644
index 00000000000000..6f61edb051e576
--- /dev/null
+++ b/Mathlib/Data/Finite/Option.lean
@@ -0,0 +1,23 @@
+/-
+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.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⟩
diff --git a/Mathlib/Data/Finite/Subtype.lean b/Mathlib/Data/Finite/Subtype.lean
new file mode 100644
index 00000000000000..3095571b4d4d1e
--- /dev/null
+++ b/Mathlib/Data/Finite/Subtype.lean
@@ -0,0 +1,20 @@
+/-
+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.Option
+
+/-!
+# `Finite`ness conditions on subtypes
+-/
+
+public section
+
+/-- The subtype of terms not equal to a given term is finite if and only if the type is finite. -/
+@[simp]
+theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by
+  classical
+  rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff]
diff --git a/Mathlib/Data/Finite/Units.lean b/Mathlib/Data/Finite/Units.lean
new file mode 100644
index 00000000000000..8a0f08e0032898
--- /dev/null
+++ b/Mathlib/Data/Finite/Units.lean
@@ -0,0 +1,29 @@
+/-
+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.Algebra.GroupWithZero.Units.Equiv
+public import Mathlib.Data.Finite.Subtype
+
+/-!
+# `Finite`ness conditions for `Units` of `GroupWithZero`
+-/
+
+public section
+
+/-- `Units` of a `GroupWithZero` are finite if and only if the `GroupWithZero` is finite. -/
+@[simp]
+theorem Units.finite_iff₀ {G : Type*} [GroupWithZero G] : Finite Gˣ ↔ Finite G := by
+  rw [unitsEquivNeZero.finite_iff, Subtype.finite_ne_iff]
+
+/-- `Units` of a `GroupWithZero` are infinite if and only if the `GroupWithZero` is infinite. -/
+@[simp]
+theorem Units.infinite_iff₀ {G : Type*} [GroupWithZero G] : Infinite Gˣ ↔ Infinite G := by
+  simpa only [not_finite_iff_infinite] using Units.finite_iff₀ (G := G).not
+
+/-- If a `GroupWithZero` is infinite then its `Units` are finite. -/
+instance {G : Type*} [GroupWithZero G] [hG : Infinite G] : Infinite Gˣ :=
+  Units.infinite_iff₀.2 ‹_›