Theorems · Definition · geometry

AffineSubspace.direction

{k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → AffineSubspace k P → Submodule k V

The direction of an affine subspace is the submodule spanned by the pairwise differences of points. (Except in the case of an empty affine subspace, where the direction is the zero submodule, every vector in the direction is the difference of two points in the affine subspace.) This can also be used to reinterpret an affine subspace that contains zero as a submodule, see direction_eq_self_iff_zero_mem.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Cited by

339 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 135 definitions · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor