Dimensions of affine spaces

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

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