coe_add — Mathlib

English

There is a canonical additive commutative group structure on the set of affine maps to a vector space: the operations are pointwise and agree with the natural linear-algebraic operations.

Русский

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

LaTeX

$$$\mathrm{Aff}_k(P_1,V_2) \cong (\text{AddCommGroup})$ с операциями сложения, нуля и тождественным элементом, определяемыми по точкам p.$$

Lean4

@[simp, norm_cast]
theorem coe_add (f g : P1 →ᵃ[k] V2) : ⇑(f + g) = f + g :=
  rfl

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