vsub_linear — Mathlib

English

The set of affine maps P1 →ᵃ[k] V2 forms an additive commutative group with pointwise operations.

Русский

Множество аффинных отображений образует аддитивную коммутативную группу с точечно определяемыми операциями.

LaTeX

$$$\text{AddCommGroup}(P_1 \to^{\mathrm{aff}}_k V_2)$ with pointwise operations$$

Lean4

@[simp]
theorem vsub_linear (f g : P1 →ᵃ[k] P2) : (f -ᵥ g).linear = f.linear - g.linear :=
  rfl

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