smul_linear — Mathlib

English

For any t ∈ R and affine map f, the linear part respects smul: (t • f).linear = t • f.linear.

Русский

Для любого t ∈ R и аффинного отображения f линейная часть сохраняет скалярное умножение: (t • f).linear = t • f.linear.

LaTeX

$$$\forall t\in R,\ f:\,P_1 \to^{\mathrm{aff}}_k V_2,\quad (t\cdot f)_{\mathrm{linear}} = t\cdot f_{\mathrm{linear}}$$$

Lean4

@[simp]
theorem smul_linear (t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear :=
  rfl

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