Theorems · Theorem · geometry

AffineMap.decomp

∀ {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddCommGroup V2] [inst_4 : Module k V2] (f : V1 →ᵃ[k] V2), ⇑f = ⇑f.linear + fun x => f 0

Decomposition of an affine map in the special case when the point space and vector space are the same.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

3 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModule