noncomputable def maxCosetDim (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (A : Set V) : ℕ

Equations

• maxCosetDim K V A = sSup {x : ℕ | ∃ (S : AffineSubspace K V) (_ : ↑S ⊆ A), Module.finrank K ↥S.direction = x}