noncomputable def AffineSpace.finrank (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : ℕ

The dimension of the affine span over ℤ of a subset of an additive group.

Equations

• AffineSpace.finrank k s = (vectorSpan k s).finrank

@[simp]

theorem AffineSpace.finrank_vadd_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) (v : V) : finrank k (v +ᵥ s) = finrank k s

@[simp]

theorem AffineSpace.finrank_empty (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] : finrank k ∅ = 0

theorem AffineSpace.finrank_le_submoduleFinrank {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {S : Submodule k V} [StrongRankCondition k] [Module.Finite k ↥S] (q : P) (hs : ∀ p ∈ s, p -ᵥ q ∈ S) : finrank k s ≤ S.finrank

theorem AffineSpace.finrank_le_moduleFinrank {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [StrongRankCondition k] [Module.Finite k V] : finrank k s ≤ Module.finrank k V