Theorems · Definition · geometry

AffineSubspace.shift

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

AffineSubspace.shift s c r is an affine subspace parallel to s, where an arbitrary point on s is moved towards c with linear interpolation by r. When r = 0, that point is moved onto c. When r = 1, that point stays at the original position. A different choice of the point will not affect the output (See AffineSubspace.shift_eq). We define AffineSubspace.shift ⊥ c r = ⊥ (See AffineSubspace.shift_bot).

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Cited by

12 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupAddTorsorModule