constVSub — Mathlib

English

The map v ↦ v +ᵥ b is an affine equivalence between a vector space V and itself translated by b.

Русский

Отображение v ↦ v +ᵥ b является аффинным эквивалентом между векторным пространством V и самим собой со сдвигом на b.

LaTeX

$$$\mathrm{vaddConst}_{b} : V_1 \to^a_k P_1, \quad v \mapsto p_0 +_v v$$$

Lean4

/-- `p' ↦ p -ᵥ p'` as an equivalence. -/
def constVSub (p : P₁) : P₁ ≃ᵃ[k] V₁ where
  toEquiv := Equiv.constVSub p
  linear := LinearEquiv.neg k
  map_vadd' p' v := by simp [vsub_vadd_eq_vsub_sub, neg_add_eq_sub]

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