diff --git a/Polyhedral.lean b/Polyhedral.lean
index 53d06d22..0fe8921c 100644
--- a/Polyhedral.lean
+++ b/Polyhedral.lean
@@ -70,11 +70,14 @@ public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.No
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineMap
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Set.FiniteDimensional
 public import Polyhedral.Mathlib.LinearAlgebra.BilinearMap
 public import Polyhedral.Mathlib.LinearAlgebra.Dual.Basis
 public import Polyhedral.Mathlib.RingTheory.Finiteness.Cofinite
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean
index 3d3fbf9f..9ca7bf49 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Basic.lean
@@ -97,6 +97,20 @@ protected lemma prod {P₂ : Set Y} (hP₁ : IsPolytope R P₁) (hP₂ : IsPolyt
 
 end Semiring
 
+section Ring
+
+variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
+variable [ConvexSpace R X]
+variable [AddCommGroup V] [Module R V] [AddTorsor V X] [IsAffineConvexSpace R V X]
+
+/-- Every polytope has finite-dimensional affine span, even in an infinite-dimensional
+ambient space. -/
+theorem finDim {P : Set X} (hP : IsPolytope R P) : Affine.FinDim R P := by
+  obtain ⟨t, rfl⟩ := hP
+  exact (Affine.FinDim.finset t).convexHull
+
+end Ring
+
 section Field
 
 variable [Field R] [PartialOrder R] [IsStrictOrderedRing R]
diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean
index cfa2a745..32cd9f6a 100644
--- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean
+++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Hull.lean
@@ -3,6 +3,7 @@ module
 public import Polyhedral.Mathlib.Geometry.Convex.AffineMap.Module
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 public import Polyhedral.Mathlib.Geometry.Convex.Hull
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Set.FiniteDimensional
 
 public section
 
@@ -28,6 +29,17 @@ theorem vectorSpan_convexHull (s : Set A) :
     vectorSpan R (convexHull R s : Set A) = vectorSpan R s := by
   rw [← direction_affineSpan, affineSpan_convexHull, direction_affineSpan]
 
+/-- Taking the convex hull preserves finite-dimensionality of a set. -/
+@[simp]
+theorem finDim_convexHull_iff (s : Set A) :
+    Affine.FinDim R (convexHull R s : Set A) ↔ Affine.FinDim R s := by
+  unfold Affine.FinDim
+  rw [vectorSpan_convexHull]
+
+theorem _root_.Affine.FinDim.convexHull {s : Set A} (hs : Affine.FinDim R s) :
+    Affine.FinDim R (convexHull R s : Set A) :=
+  (finDim_convexHull_iff s).mpr hs
+
 variable [ConvexSpace R V] [IsModuleConvexSpace R V]
 
 @[simp]
diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean
new file mode 100644
index 00000000..0b91a8ed
--- /dev/null
+++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/FiniteDimensional.lean
@@ -0,0 +1,248 @@
+/-
+Copyright (c) 2026 Martin Winter. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Winter
+-/
+module
+
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+
+/-!
+# Finite-dimensional affine subspaces
+
+`AffineSubspace.FinDim s` means that the direction of `s` is a finite module.
+Over a division ring this is finite-dimensionality; over a general ring it is finite generation.
+It abbreviates `Module.Finite`, as does `FiniteDimensional` for vector spaces.
+The closure lemmas in this file take explicit proofs of this predicate and register no
+additional instances. A proof can still be installed locally with `let := hs` to use
+Mathlib's API for `s.direction`, `s.dim`, and `s.finDim`.
+
+The empty subspace is finite-dimensional, although its affine dimension is `⊥`.
+Infinite-dimensional subspaces have the junk value `finDim = 0`; use `dim < ℵ₀` to
+characterize finite-dimensionality instead.
+
+Finite-dimensionality of an affine space is expressed separately by
+`AffineSpace.FiniteDimensional K P`. For a nonempty subspace `s`, the two notions agree when
+`s` is viewed as an affine space modeled on `s.direction`.
+-/
+
+@[expose] public section
+
+namespace AffineSubspace
+
+variable {K V P : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V P]
+
+/-- An affine subspace is finite-dimensional if its direction is a finite module.
+In particular, the empty affine subspace is finite-dimensional. -/
+abbrev FinDim {R V A : Type*} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V A]
+    (s : AffineSubspace R A) : Prop :=
+  Module.Finite R s.direction
+
+variable {s t : AffineSubspace K P}
+
+theorem finDim_iff_direction :
+    s.FinDim ↔ _root_.FiniteDimensional K s.direction := Iff.rfl
+
+/-- A nonempty affine subspace has the same finite-dimensionality as its underlying affine
+space. This comparison is a theorem, not an instance. -/
+theorem finDim_iff_affineSpace (s : AffineSubspace K P) [Nonempty s] :
+    s.FinDim ↔ AffineSpace.FiniteDimensional K s := Iff.rfl
+
+theorem dim_eq_affine_dim (s : AffineSubspace K P) [Nonempty s] :
+    s.dim = (AffineSpace.dim K s : WithBot Cardinal) :=
+  dim_eq_rank (nonempty_iff_ne_bot s |>.mp (Set.nonempty_coe_sort.mp inferInstance))
+
+theorem finDim_eq_affine_finDim (s : AffineSubspace K P) [Nonempty s] :
+    s.finDim = (AffineSpace.finDim K s : WithBot ℕ) :=
+  finDim_eq_finrank (nonempty_iff_ne_bot s |>.mp (Set.nonempty_coe_sort.mp inferInstance))
+
+@[simp]
+theorem finDim_top_iff :
+    (⊤ : AffineSubspace K P).FinDim ↔ _root_.FiniteDimensional K V := by
+  unfold FinDim
+  rw [direction_top]
+  exact ⟨fun h ↦ by
+    let := h
+    exact Submodule.topEquiv.finiteDimensional, fun h ↦ by
+    let := h
+    infer_instance⟩
+
+@[simp]
+theorem finDim_toAffineSubspace_iff (S : Submodule K V) :
+    S.toAffineSubspace.FinDim ↔ _root_.FiniteDimensional K S := by
+  unfold FinDim
+  rw [Submodule.toAffineSubspace_direction]
+
+theorem FinDim.toAffineSubspace (S : Submodule K V)
+    (hS : _root_.FiniteDimensional K S) : S.toAffineSubspace.FinDim :=
+  (finDim_toAffineSubspace_iff S).mpr hS
+
+theorem FinDim.mk' (p : P) (S : Submodule K V)
+    (hS : _root_.FiniteDimensional K S) : (mk' p S).FinDim := by
+  unfold FinDim
+  rw [direction_mk']
+  exact hS
+
+/-- Every affine subspace of a finite-dimensional ambient space is finite-dimensional. -/
+theorem FinDim.of_finiteDimensional
+    [AffineSpace.FiniteDimensional K P] (s : AffineSubspace K P) : s.FinDim :=
+  inferInstanceAs (_root_.FiniteDimensional K s.direction)
+
+theorem FinDim.bot : (⊥ : AffineSubspace K P).FinDim := by
+  unfold FinDim
+  rw [direction_bot]
+  infer_instance
+
+/-- Finite-dimensionality descends to affine subspaces. -/
+theorem FinDim.mono (ht : t.FinDim) (h : s ≤ t) :
+    s.FinDim := by
+  let := ht
+  exact Submodule.finiteDimensional_of_le (direction_le h)
+
+theorem FinDim.inf_left (s t : AffineSubspace K P) (hs : s.FinDim) :
+    (s ⊓ t).FinDim :=
+  FinDim.mono hs inf_le_left
+
+theorem FinDim.inf_right (s t : AffineSubspace K P) (ht : t.FinDim) :
+    (s ⊓ t).FinDim :=
+  FinDim.mono ht inf_le_right
+
+/-- An indexed intersection is finite-dimensional if one of its members is. -/
+theorem FinDim.iInf {ι : Sort*} (S : ι → AffineSubspace K P) (i : ι)
+    (hi : (S i).FinDim) : (⨅ j, S j).FinDim :=
+  FinDim.mono hi (iInf_le S i)
+
+theorem FinDim.finset_sup {ι : Type*} (I : Finset ι)
+    (S : ι → AffineSubspace K P) (hS : ∀ i ∈ I, (S i).FinDim) :
+    (I.sup S).FinDim := by
+  refine Finset.sup_induction FinDim.bot ?_ hS
+  intro s hs t ht
+  let := hs
+  let := ht
+  infer_instance
+
+theorem FinDim.iSup {ι : Sort*} [Finite ι] (S : ι → AffineSubspace K P)
+    (hS : ∀ i, (S i).FinDim) : (⨆ i, S i).FinDim := by
+  classical
+  let := Fintype.ofFinite (PLift ι)
+  simpa only [Finset.sup_univ_eq_iSup, iSup_plift_down] using
+    FinDim.finset_sup Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down)
+
+/-- A singleton is finite-dimensional, even in an infinite-dimensional ambient space. -/
+theorem FinDim.singleton (p : P) : ({p} : AffineSubspace K P).FinDim :=
+  inferInstance
+
+/-- Binary joins preserve finite-dimensionality. -/
+theorem FinDim.sup (hs : s.FinDim)
+    (ht : t.FinDim) : (s ⊔ t).FinDim := by
+  let := hs
+  let := ht
+  infer_instance
+
+/-- The affine span of a finite set is finite-dimensional. -/
+theorem FinDim.affineSpan_of_finite {S : Set P} (hS : S.Finite) :
+    (affineSpan K S).FinDim :=
+  finiteDimensional_direction_affineSpan_of_finite K hS
+
+theorem FinDim.affineSpan_finset (S : Finset P) :
+    (affineSpan K (S : Set P)).FinDim :=
+  FinDim.affineSpan_of_finite S.finite_toSet
+
+/-- The affine span of a subset of a finite-dimensional subspace is finite-dimensional. -/
+theorem FinDim.affineSpan_of_subset (hs : s.FinDim) {S : Set P}
+    (hS : S ⊆ s) : (affineSpan K S).FinDim :=
+  FinDim.mono hs (affineSpan_le.mpr hS)
+
+section Map
+
+variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q]
+
+theorem FinDim.map (hs : s.FinDim) (f : P →ᵃ[K] Q) :
+    (s.map f).FinDim := by
+  let := hs
+  infer_instance
+
+/-- Finite-dimensionality descends along an injective affine map. -/
+theorem FinDim.of_map {f : P →ᵃ[K] Q} (hf : Function.Injective f)
+    (hs : (s.map f).FinDim) : s.FinDim := by
+  have : _root_.FiniteDimensional K (s.direction.map f.linear) := by
+    rw [← map_direction]
+    exact hs
+  exact (Submodule.equivMapOfInjective f.linear
+    (f.linear_injective_iff.mpr hf) s.direction).symm.finiteDimensional
+
+theorem finDim_map_iff {f : P →ᵃ[K] Q} (hf : Function.Injective f) :
+    (s.map f).FinDim ↔ s.FinDim := by
+  constructor
+  · exact FinDim.of_map hf
+  · exact fun h ↦ FinDim.map h f
+
+/-- An injective affine preimage of a finite-dimensional subspace is finite-dimensional. -/
+theorem FinDim.comap_of_injective {f : P →ᵃ[K] Q} (hf : Function.Injective f)
+    (t : AffineSubspace K Q) (ht : t.FinDim) : (t.comap f).FinDim :=
+  FinDim.of_map hf (FinDim.mono ht (map_comap_le f t))
+
+@[simp]
+theorem finDim_map_equiv_iff (e : P ≃ᵃ[K] Q) :
+    (s.map e.toAffineMap).FinDim ↔ s.FinDim :=
+  finDim_map_iff e.injective
+
+end Map
+
+/-- Finite-dimensional affine subspaces are precisely the affine spans of finite sets. -/
+theorem finDim_iff_exists_finite_affineSpan :
+    s.FinDim ↔ ∃ S : Set P, S.Finite ∧ affineSpan K S = s := by
+  constructor
+  · intro hs
+    let := hs
+    obtain ⟨S, -, hS, hI⟩ := exists_affineIndependent K V (s : Set P)
+    have hspan : affineSpan K S = s := hS.trans (affineSpan_coe s)
+    have : (affineSpan K S).FinDim := hspan ▸ hs
+    have : _root_.FiniteDimensional K (vectorSpan K (Set.range ((↑) : S → P))) := by
+      rw [Subtype.range_coe, ← direction_affineSpan]
+      exact (inferInstance : (affineSpan K S).FinDim)
+    exact ⟨S, (finiteDimensional_iff_setFinite K hI).mp inferInstance, hspan⟩
+  · rintro ⟨S, hS, rfl⟩
+    exact FinDim.affineSpan_of_finite hS
+
+theorem finDim_iff_exists_finset_affineSpan :
+    s.FinDim ↔ ∃ S : Finset P, affineSpan K (S : Set P) = s := by
+  classical
+  rw [finDim_iff_exists_finite_affineSpan]
+  exact ⟨fun ⟨S, hS, hspan⟩ ↦ ⟨hS.toFinset, by simpa using hspan⟩,
+    fun ⟨S, hspan⟩ ↦ ⟨S, S.finite_toSet, hspan⟩⟩
+
+/-- The cardinal-valued dimension detects finite-dimensionality, including for `⊥`. -/
+theorem finDim_iff_dim_lt_aleph0 :
+    s.FinDim ↔ s.dim < (Cardinal.aleph0 : WithBot Cardinal) :=
+  finite_iff_dim_lt_aleph0 s
+
+/-- In finite dimension, the cardinal dimension is the natural dimension cast to cardinals.
+This formulation also applies to the empty subspace. -/
+theorem dim_eq_map_finDim (hs : s.FinDim) :
+    s.dim = s.finDim.map (fun n : ℕ ↦ (n : Cardinal)) := by
+  let := hs
+  rcases eq_or_ne s ⊥ with rfl | hbot
+  · simp
+  rw [dim_eq_rank hbot, finDim_eq_finrank hbot, WithBot.map_natCast, WithBot.coe_inj]
+  exact (Module.finrank_eq_rank' (K := K) (V := s.direction)).symm
+
+/-- A finite-dimensional affine subspace is determined by inclusion and finite dimension. -/
+theorem eq_of_le_of_finDim_eq (ht : t.FinDim) (h : s ≤ t)
+    (hd : s.finDim = t.finDim) : s = t := by
+  let := ht
+  by_contra hne
+  exact (ne_of_lt (finDim_strictMono (lt_of_le_of_ne h hne))) hd
+
+theorem finDim_eq_iff_eq_of_le (ht : t.FinDim) (h : s ≤ t) :
+    s.finDim = t.finDim ↔ s = t :=
+  ⟨eq_of_le_of_finDim_eq ht h, fun h ↦ congrArg finDim h⟩
+
+theorem lt_iff_finDim_lt_of_le (ht : t.FinDim) (h : s ≤ t) :
+    s < t ↔ s.finDim < t.finDim := by
+  let := ht
+  refine ⟨finDim_strictMono, fun hd ↦ lt_of_le_of_ne h ?_⟩
+  intro heq
+  exact (ne_of_lt hd) (congrArg finDim heq)
+
+end AffineSubspace
diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
new file mode 100644
index 00000000..04cd4ffa
--- /dev/null
+++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2026 Martin Winter. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Winter
+-/
+module
+
+public import Mathlib.LinearAlgebra.AffineSpace.Dimension
+public import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+public import Mathlib.Data.Fintype.Card
+
+/-!
+# Finite-dimensional affine spaces
+
+`AffineSpace.FiniteDimensional K P` expresses finite-dimensionality of an affine space `P`
+over `K`. Its model vector space `V` is inferred from `[AddTorsor V P]`.
+The definition abbreviates `FiniteDimensional K V`, so the two typeclass assumptions
+are interchangeable and all of Mathlib's instances on model vector spaces apply directly.
+In particular, vector spaces, products, and nonempty affine subspaces inherit finite dimension.
+No conversion instances are needed in either direction.
+
+`AffineSpace.dim K P` and `AffineSpace.finDim K P` are the dimensions of the model vector space.
+An affine space is nonempty, so these do not need the bottom value used by
+`AffineSubspace.dim` and `AffineSubspace.finDim`. As with `Module.finrank`, `finDim` has
+the junk value zero in infinite dimension.
+
+The predicate on affine subspaces is kept separately in
+`AffineSpace/AffineSubspace/FiniteDimensional.lean`; that file provides explicit closure
+lemmas and a comparison for a nonempty subspace viewed as an affine space.
+-/
+
+@[expose] public section
+
+namespace AffineSpace
+
+/-- An affine space is finite-dimensional when its model vector space is finite-dimensional. -/
+abbrev FiniteDimensional (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V]
+    [Module K V] [AddTorsor V P] : Prop :=
+  _root_.FiniteDimensional K V
+
+/-- The cardinal dimension of an affine space is the rank of its model vector space. -/
+noncomputable def dim (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V]
+    [Module K V] [AddTorsor V P] : Cardinal :=
+  Module.rank K V
+
+/-- The finite dimension of an affine space, with the junk value zero in infinite dimension. -/
+noncomputable def finDim (K P : Type*) {V : Type*} [DivisionRing K] [AddCommGroup V]
+    [Module K V] [AddTorsor V P] : ℕ :=
+  Module.finrank K V
+
+variable {K V P : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V P]
+
+theorem finiteDimensional_iff_model :
+    FiniteDimensional K P ↔ _root_.FiniteDimensional K V := Iff.rfl
+
+theorem dim_eq_rank : dim K P = Module.rank K V := rfl
+
+theorem finDim_eq_finrank : finDim K P = Module.finrank K V := rfl
+
+@[simp]
+theorem dim_eq_zero_iff : dim K P = 0 ↔ Subsingleton P :=
+  (rank_zero_iff (R := K) (M := V)).trans (AddTorsor.subsingleton_iff V P)
+
+@[simp]
+theorem dim_top : (⊤ : AffineSubspace K P).dim = (dim K P : WithBot Cardinal) :=
+  by rw [AffineSubspace.dim_eq_rank (by simp), AffineSubspace.direction_top,
+    _root_.rank_top]; rfl
+
+@[simp]
+theorem finDim_top : (⊤ : AffineSubspace K P).finDim = (finDim K P : WithBot ℕ) := by
+  rw [AffineSubspace.finDim_eq_finrank (by simp), AffineSubspace.direction_top,
+    _root_.finrank_top]
+  rfl
+
+theorem finiteDimensional_iff_dim_lt_aleph0 :
+    FiniteDimensional K P ↔ dim K P < Cardinal.aleph0 :=
+  Module.rank_lt_aleph0_iff.symm
+
+theorem finDim_eq_zero_of_not_finiteDimensional (h : ¬FiniteDimensional K P) :
+    finDim K P = 0 :=
+  Module.finrank_of_not_finite h
+
+namespace FiniteDimensional
+
+variable [FiniteDimensional K P]
+
+theorem dim_lt_aleph0 : dim K P < Cardinal.aleph0 := Module.rank_lt_aleph0 K V
+
+theorem finDim_eq_dim : (finDim K P : Cardinal) = dim K P :=
+  Module.finrank_eq_rank' K V
+
+@[simp]
+theorem finDim_eq_zero_iff : finDim K P = 0 ↔ Subsingleton P :=
+  (Module.finrank_zero_iff (R := K) (M := V)).trans (AddTorsor.subsingleton_iff V P)
+
+/-- A finite-dimensional affine space admits a finite affine basis. -/
+theorem exists_affineBasis : Nonempty (AffineBasis (Fin (finDim K P + 1)) K P) :=
+  AffineBasis.exists_affineBasis_of_finiteDimensional (Fintype.card_fin _)
+
+/-- A finite-dimensional affine space is generated by finitely many points. -/
+theorem exists_finset_affineSpan : ∃ S : Finset P, affineSpan K (S : Set P) = ⊤ := by
+  classical
+  obtain ⟨b⟩ := exists_affineBasis (K := K) (P := P)
+  exact ⟨Finset.univ.image b, by simpa only [Finset.coe_image, Finset.coe_univ,
+    Set.image_univ] using b.tot⟩
+
+section Map
+
+variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q]
+
+omit [FiniteDimensional K P] in
+/-- An affine space injecting into a finite-dimensional affine space is finite-dimensional. -/
+theorem of_injective [FiniteDimensional K Q] (f : P →ᵃ[K] Q)
+    (hf : Function.Injective f) : FiniteDimensional K P :=
+  _root_.FiniteDimensional.of_injective f.linear (f.linear_injective_iff.mpr hf)
+
+/-- A surjective affine image of a finite-dimensional affine space is finite-dimensional. -/
+theorem of_surjective (f : P →ᵃ[K] Q) (hf : Function.Surjective f) :
+    FiniteDimensional K Q :=
+  _root_.FiniteDimensional.of_surjective f.linear (f.linear_surjective_iff.mpr hf)
+
+/-- Finite-dimensionality is preserved by an affine equivalence. -/
+theorem of_equiv (e : P ≃ᵃ[K] Q) : FiniteDimensional K Q :=
+  e.linear.finiteDimensional
+
+omit [FiniteDimensional K P] in
+theorem finDim_le_of_injective [FiniteDimensional K Q] (f : P →ᵃ[K] Q)
+    (hf : Function.Injective f) : finDim K P ≤ finDim K Q :=
+  LinearMap.finrank_le_finrank_of_injective (f.linear_injective_iff.mpr hf)
+
+theorem finDim_le_of_surjective (f : P →ᵃ[K] Q) (hf : Function.Surjective f) :
+    finDim K Q ≤ finDim K P :=
+  LinearMap.finrank_le_finrank_of_surjective (f.linear_surjective_iff.mpr hf)
+
+end Map
+
+end FiniteDimensional
+
+/-- An affine space is finite-dimensional exactly when a finite set of points spans it. -/
+theorem finiteDimensional_iff_exists_finset_affineSpan :
+    FiniteDimensional K P ↔ ∃ S : Finset P, affineSpan K (S : Set P) = ⊤ := by
+  constructor
+  · intro h
+    let := h
+    exact FiniteDimensional.exists_finset_affineSpan
+  · rintro ⟨S, hS⟩
+    have h : _root_.FiniteDimensional K (affineSpan K (S : Set P)).direction :=
+      finiteDimensional_direction_affineSpan_of_finite K S.finite_toSet
+    rw [hS, AffineSubspace.direction_top] at h
+    let := h
+    exact Submodule.topEquiv.finiteDimensional
+
+section Equiv
+
+variable {W Q : Type*} [AddCommGroup W] [Module K W] [AddTorsor W Q]
+
+theorem finiteDimensional_iff_of_equiv (e : P ≃ᵃ[K] Q) :
+    FiniteDimensional K P ↔ FiniteDimensional K Q := by
+  constructor
+  · intro h
+    let := h
+    exact FiniteDimensional.of_equiv e
+  · intro h
+    let := h
+    exact FiniteDimensional.of_equiv e.symm
+
+theorem finDim_eq_of_equiv (e : P ≃ᵃ[K] Q) : finDim K P = finDim K Q :=
+  e.linear.finrank_eq
+
+end Equiv
+
+end AffineSpace
diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean
new file mode 100644
index 00000000..215cc972
--- /dev/null
+++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Set/FiniteDimensional.lean
@@ -0,0 +1,314 @@
+/-
+Copyright (c) 2026 Martin Winter. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Winter
+-/
+module
+
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.FiniteDimensional
+public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
+public import Mathlib.Algebra.Group.Pointwise.Set.Finite
+public import Mathlib.Algebra.Order.SuccPred.WithBot
+
+/-!
+# Finite-dimensional subsets of affine spaces
+
+`Affine.FinDim R s` means that the affine span of a set `s` has finitely generated
+direction. Over a division ring this is finite-dimensionality. The abbreviation is
+definitionally `Module.Finite R (vectorSpan R s)`, so existing assumptions on the vector
+span can be written `[Affine.FinDim R s]` without conversion instances.
+
+This is a predicate, distinct from the numerical dimension `Affine.finrank R s` and
+`(affineSpan R s).finDim`. The empty set satisfies the predicate and its affine span has
+dimension `⊥`. Closure lemmas take explicit proofs and register no additional instances.
+
+The API includes affine-span and image invariance, finite unions, descent to subsets over
+a division ring, dimension comparisons, and finite independent spanning subsets with
+cardinality `(affineSpan R s).finDim.succ`. The last formulation also covers the empty set
+and is suited to homogenization and grading of polytope faces.
+-/
+
+@[expose] public section
+
+namespace Affine
+
+/-- A subset of an affine space is finite-dimensional when its vector span is a finite module.
+The definition also applies over rings, where it expresses finite generation. -/
+abbrev FinDim (R : Type*) {V A : Type*} [Ring R] [AddCommGroup V] [Module R V]
+    [AddTorsor V A] (s : Set A) : Prop :=
+  Module.Finite R (vectorSpan R s)
+
+section Ring
+
+variable {R V A : Type*} [Ring R] [AddCommGroup V] [Module R V] [AddTorsor V A]
+variable {s t : Set A}
+
+theorem finDim_iff_vectorSpan : FinDim R s ↔ Module.Finite R (vectorSpan R s) := Iff.rfl
+
+@[simp]
+theorem finDim_coe_iff (S : AffineSubspace R A) : FinDim R (S : Set A) ↔ S.FinDim :=
+  Iff.rfl
+
+/-- View a finite-dimensional affine subspace as a finite-dimensional subset. -/
+theorem _root_.AffineSubspace.FinDim.coe {S : AffineSubspace R A} (hS : S.FinDim) :
+    FinDim R (S : Set A) :=
+  (finDim_coe_iff S).mpr hS
+
+/-- Finite-dimensionality is exactly finite-dimensionality of the affine span. -/
+theorem finDim_iff_affineSpan : FinDim R s ↔ (_root_.affineSpan R s).FinDim := by
+  unfold FinDim AffineSubspace.FinDim
+  rw [direction_affineSpan]
+
+@[simp]
+theorem finDim_affineSpan_iff : FinDim R (_root_.affineSpan R s : Set A) ↔ FinDim R s := by
+  rw [finDim_coe_iff, ← finDim_iff_affineSpan]
+
+theorem finDim_congr (h : _root_.affineSpan R s = _root_.affineSpan R t) :
+    FinDim R s ↔ FinDim R t := by
+  rw [finDim_iff_affineSpan, h, ← finDim_iff_affineSpan]
+
+namespace FinDim
+
+theorem affineSpan (hs : FinDim R s) : (_root_.affineSpan R s).FinDim :=
+  finDim_iff_affineSpan.mp hs
+
+theorem of_affineSpan_eq (hs : FinDim R s) (h : _root_.affineSpan R t = _root_.affineSpan R s) :
+    FinDim R t :=
+  (finDim_congr h).mpr hs
+
+/-- Every finite set of points is finite-dimensional, over any ring. -/
+theorem of_finite (hs : s.Finite) : FinDim R s := by
+  unfold FinDim
+  rw [vectorSpan_def]
+  exact Module.Finite.span_of_finite R (hs.vsub hs)
+
+theorem finset (S : Finset A) : FinDim R (S : Set A) := of_finite S.finite_toSet
+
+@[simp]
+theorem empty : FinDim R (∅ : Set A) := of_finite Set.finite_empty
+
+@[simp]
+theorem singleton (p : A) : FinDim R ({p} : Set A) := of_finite (Set.finite_singleton p)
+
+theorem of_subsingleton (hs : s.Subsingleton) : FinDim R s := of_finite hs.finite
+
+theorem range {ι : Sort*} [Finite ι] (p : ι → A) : FinDim R (Set.range p) :=
+  of_finite (Set.finite_range p)
+
+/-- A finite union of finite-dimensional sets is finite-dimensional. The joining direction
+between two disjoint affine spans is included in the proof. -/
+theorem union (hs : FinDim R s) (ht : FinDim R t) : FinDim R (s ∪ t) := by
+  rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩
+  · simpa using ht
+  rcases t.eq_empty_or_nonempty with rfl | ⟨q, hq⟩
+  · simpa using hs
+  have : Module.Finite R (_root_.affineSpan R s).direction := hs.affineSpan
+  have : Module.Finite R (_root_.affineSpan R t).direction := ht.affineSpan
+  unfold FinDim
+  rw [← direction_affineSpan, AffineSubspace.span_union,
+    AffineSubspace.direction_sup (mem_affineSpan R hp) (mem_affineSpan R hq)]
+  infer_instance
+
+theorem insert (hs : FinDim R s) (p : A) : FinDim R (insert p s) := by
+  simpa only [Set.singleton_union] using (singleton p).union hs
+
+theorem biUnion {ι : Type*} (I : Finset ι) (S : ι → Set A)
+    (hS : ∀ i ∈ I, FinDim R (S i)) : FinDim R (⋃ i ∈ I, S i) := by
+  classical
+  induction I using Finset.induction_on with
+  | empty => simp
+  | @insert i I hi ih =>
+    rw [Finset.set_biUnion_insert]
+    exact (hS i (Finset.mem_insert_self _ _)).union
+      (ih (fun j hj ↦ hS j (Finset.mem_insert_of_mem hj)))
+
+theorem iUnion {ι : Sort*} [Finite ι] (S : ι → Set A) (hS : ∀ i, FinDim R (S i)) :
+    FinDim R (⋃ i, S i) := by
+  classical
+  let := Fintype.ofFinite (PLift ι)
+  simpa only [Finset.mem_univ, Set.iUnion_true, Set.iUnion_plift_down] using
+    biUnion Finset.univ (fun i : PLift ι ↦ S i.down) (fun i _ ↦ hS i.down)
+
+section Image
+
+variable {W B : Type*} [AddCommGroup W] [Module R W] [AddTorsor W B]
+
+theorem image (hs : FinDim R s) (f : A →ᵃ[R] B) : FinDim R (f '' s) := by
+  let := hs
+  unfold FinDim
+  rw [← f.map_vectorSpan]
+  infer_instance
+
+theorem of_image {f : A →ᵃ[R] B} (hs : FinDim R (f '' s)) (hf : Function.Injective f) :
+    FinDim R s := by
+  have : Module.Finite R ((vectorSpan R s).map f.linear) := by
+    rw [f.map_vectorSpan]
+    exact hs
+  exact Module.Finite.equiv
+    (Submodule.equivMapOfInjective f.linear (f.linear_injective_iff.mpr hf) _).symm
+
+end Image
+
+end FinDim
+
+section Image
+
+variable {W B : Type*} [AddCommGroup W] [Module R W] [AddTorsor W B]
+
+theorem finDim_image_iff {f : A →ᵃ[R] B} (hf : Function.Injective f) :
+    FinDim R (f '' s) ↔ FinDim R s :=
+  ⟨fun h ↦ h.of_image hf, fun h ↦ h.image f⟩
+
+@[simp]
+theorem finDim_image_equiv_iff (e : A ≃ᵃ[R] B) : FinDim R (e '' s) ↔ FinDim R s :=
+  finDim_image_iff (f := e.toAffineMap) e.injective
+
+end Image
+
+end Ring
+
+section DivisionRing
+
+variable {K V A : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V A]
+variable {s t : Set A}
+
+@[simp]
+theorem finDim_univ_iff :
+    FinDim K (Set.univ : Set A) ↔ AffineSpace.FiniteDimensional K A := by
+  rw [finDim_iff_affineSpan, AffineSubspace.span_univ,
+    AffineSubspace.finDim_top_iff]
+
+@[simp]
+theorem finDim_union_iff : FinDim K (s ∪ t) ↔ FinDim K s ∧ FinDim K t := by
+  constructor
+  · intro h
+    let := h
+    exact ⟨Submodule.finiteDimensional_of_le
+      (vectorSpan_mono K (Set.subset_union_left : s ⊆ s ∪ t)),
+      Submodule.finiteDimensional_of_le
+      (vectorSpan_mono K (Set.subset_union_right : t ⊆ s ∪ t))⟩
+  · exact fun ⟨hs, ht⟩ ↦ hs.union ht
+
+theorem finDim_iff_dim_lt_aleph0 :
+    FinDim K s ↔ (_root_.affineSpan K s).dim < (Cardinal.aleph0 : WithBot Cardinal) := by
+  rw [finDim_iff_affineSpan]
+  exact AffineSubspace.finDim_iff_dim_lt_aleph0
+
+theorem finDim_iff_rank_lt_aleph0 : FinDim K s ↔ rank K s < Cardinal.aleph0 := by
+  unfold rank
+  rw [direction_affineSpan]
+  exact Module.rank_lt_aleph0_iff.symm
+
+theorem finDim_iff_exists_finite_affineSpan :
+    FinDim K s ↔ ∃ t : Set A, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s := by
+  rw [finDim_iff_affineSpan, AffineSubspace.finDim_iff_exists_finite_affineSpan]
+
+theorem finDim_iff_exists_finset_affineSpan :
+    FinDim K s ↔ ∃ t : Finset A, _root_.affineSpan K (t : Set A) = _root_.affineSpan K s := by
+  rw [finDim_iff_affineSpan, AffineSubspace.finDim_iff_exists_finset_affineSpan]
+
+namespace FinDim
+
+/-- Finite-dimensionality descends to every subset over a division ring. -/
+theorem mono (ht : FinDim K t) (h : s ⊆ t) : FinDim K s := by
+  let := ht
+  exact Submodule.finiteDimensional_of_le (vectorSpan_mono K h)
+
+theorem of_finiteDimensional [AffineSpace.FiniteDimensional K A] (s : Set A) : FinDim K s :=
+  inferInstanceAs (Module.Finite K (vectorSpan K s))
+
+theorem inter_left (hs : FinDim K s) (t : Set A) : FinDim K (s ∩ t) :=
+  hs.mono Set.inter_subset_left
+
+theorem inter_right (ht : FinDim K t) (s : Set A) : FinDim K (s ∩ t) :=
+  ht.mono Set.inter_subset_right
+
+theorem diff (hs : FinDim K s) (t : Set A) : FinDim K (s \ t) := hs.mono Set.sdiff_subset
+
+theorem finrank_mono (ht : FinDim K t) (h : s ⊆ t) : finrank K s ≤ finrank K t := by
+  let := ht
+  unfold finrank
+  rw [direction_affineSpan, direction_affineSpan]
+  exact Submodule.finrank_mono (vectorSpan_mono K h)
+
+theorem finDim_mono (ht : FinDim K t) (h : s ⊆ t) :
+    (_root_.affineSpan K s).finDim ≤ (_root_.affineSpan K t).finDim := by
+  have := ht.affineSpan
+  exact AffineSubspace.finDim_mono (affineSpan_mono K h)
+
+theorem finrank_eq_rank (hs : FinDim K s) : (finrank K s : Cardinal) = rank K s := by
+  have := hs.affineSpan
+  exact Module.finrank_eq_rank' K (_root_.affineSpan K s).direction
+
+/-- Equal dimensions and inclusion imply equality of the affine spans, not necessarily of
+the original sets. -/
+theorem affineSpan_eq_of_subset_of_finDim_eq (ht : FinDim K t) (h : s ⊆ t)
+    (hd : (_root_.affineSpan K s).finDim = (_root_.affineSpan K t).finDim) :
+    _root_.affineSpan K s = _root_.affineSpan K t :=
+  AffineSubspace.eq_of_le_of_finDim_eq ht.affineSpan (affineSpan_mono K h) hd
+
+end FinDim
+
+end DivisionRing
+
+end Affine
+
+section AffineIndependent
+
+variable {K V A : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [AddTorsor V A]
+variable {s : Set A}
+
+/-- An independent set in a finite-dimensional affine span is finite. -/
+theorem AffineIndepOn.finite_of_finDim (hi : AffineIndepOn K id s)
+    (hs : Affine.FinDim K s) : s.Finite := by
+  have h : FiniteDimensional K (vectorSpan K (Set.range ((↑) : s → A))) := by
+    rw [Subtype.range_coe]
+    exact hs
+  exact (finiteDimensional_iff_setFinite K hi).mp h
+
+/-- An independent set has one more point than its affine dimension. Using `WithBot.succ`
+also covers the empty set: the successor of its dimension `⊥` is zero. -/
+theorem AffineIndepOn.ncard_eq_succ_finDim_affineSpan (hi : AffineIndepOn K id s)
+    [hs : Affine.FinDim K s] : s.ncard = (_root_.affineSpan K s).finDim.succ := by
+  have hfinite := hi.finite_of_finDim hs
+  rcases s.eq_empty_or_nonempty with rfl | hnonempty
+  · simp
+  rw [AffineSubspace.finDim_eq_finrank
+    (by simpa [← Set.nonempty_iff_ne_empty] using hnonempty), direction_affineSpan,
+    WithBot.succ_natCast, hi.finrank_vectorSpan hfinite hnonempty]
+  exact (Nat.sub_add_cancel (Nat.succ_le_of_lt ((Set.ncard_pos hfinite).mpr hnonempty))).symm
+
+theorem AffineIndependent.ncard_eq_succ_finDim_affineSpan
+    (hi : AffineIndependent K ((↑) : s → A)) [Affine.FinDim K s] :
+    s.ncard = (_root_.affineSpan K s).finDim.succ :=
+  (show AffineIndepOn K id s from hi).ncard_eq_succ_finDim_affineSpan
+
+namespace Affine.FinDim
+
+/-- A finite-dimensional set contains a finite independent subset spanning the same affine
+subspace. Its cardinality is already expressed in terms of the original set's dimension. -/
+theorem exists_affineIndependent (hs : Affine.FinDim K s) :
+    ∃ t ⊆ s, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s ∧
+      AffineIndependent K ((↑) : t → A) ∧ t.ncard = (_root_.affineSpan K s).finDim.succ := by
+  obtain ⟨t, ht, hspan, hi⟩ := _root_.exists_affineIndependent K V s
+  have htDim : Affine.FinDim K t := hs.of_affineSpan_eq hspan
+  have hai : AffineIndepOn K id t := hi
+  let := htDim
+  refine ⟨t, ht, hai.finite_of_finDim htDim, hspan, hi, ?_⟩
+  rw [← hspan]
+  exact hai.ncard_eq_succ_finDim_affineSpan
+
+theorem exists_affineIndepOn (hs : Affine.FinDim K s) :
+    ∃ t ⊆ s, t.Finite ∧ _root_.affineSpan K t = _root_.affineSpan K s ∧
+      AffineIndepOn K id t ∧ t.ncard = (_root_.affineSpan K s).finDim.succ :=
+  hs.exists_affineIndependent
+
+theorem exists_finset_subset_affineSpan (hs : Affine.FinDim K s) :
+    ∃ t : Finset A, (t : Set A) ⊆ s ∧ _root_.affineSpan K (t : Set A) = _root_.affineSpan K s := by
+  classical
+  obtain ⟨t, ht, hfinite, hspan, -, -⟩ := hs.exists_affineIndependent
+  exact ⟨hfinite.toFinset, by simpa using ht, by simpa using hspan⟩
+
+end Affine.FinDim
+
+end AffineIndependent