id — Mathlib · SciLib

English

There exists an identity affine map id: P1 → P1 with toFun = id and linear = LinearMap.id.

Русский

Существует тождественное аффинное отображение id: P1 → P1, такое что toFun = id и линейная часть = LinearMap.id.

LaTeX

$$$id_{P_1} : P_1 \\to P_1$ является аффинным отображением с коэффициентной линейной частью равной $\\mathrm{LinearMap.id}$.$$

Lean4

/-- Identity map as an affine map. -/
nonrec def id : P1 →ᵃ[k] P1 where
  toFun := id
  linear := LinearMap.id
  map_vadd' _ _ := rfl

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