Theorems · Theorem · geometry

AffineMap.map_vadd

∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1), f (v +ᵥ p) = f.linear v +ᵥ f p

An affine map on the result of adding a vector to a point produces the same result as the linear map applied to that vector, added to the affine map applied to that point.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

17 results in Mathlib

Foundations

Depth 27 from the axioms · uses Quot.sound

Assumes

RingAddCommGroupModuleAddTorsorAddCommGroupModuleAddTorsor