Theorems · Theorem · geometry

AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial

∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P} [Nontrivial P], affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

For a non-trivial space, the affine span of a set is ⊤ iff its vector span is ⊤.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsorNontrivial