toAffineMap — Mathlib

English

The linear part of the affine map obtained from a linear map f is exactly f.

Русский

Линейная часть аффинного отображения, полученного из линейного отображения f, равна f.

LaTeX

$$$(f: V_1 \to_{} V_2) \,\mathrm{.toAffineMap}.linear = f$$$

Lean4

/-- Reinterpret a linear map as an affine map. -/
def toAffineMap : V₁ →ᵃ[k] V₂ where
  toFun := f
  linear := f
  map_vadd' p v := f.map_add v p

Похожие утверждения