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
Instances For
@[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)
:
AffineSpace.finrank k (v +ᵥ s) = AffineSpace.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]
:
AffineSpace.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)
:
AffineSpace.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]
:
AffineSpace.finrank k s ≤ Module.finrank k V