coe_vadd — Mathlib

English

The coercion of the translated basis equals the translation of the coerced basis: the indicator for v +ᵥ b equals the same addition on the function level.

Русский

Приведение к функции от переведённой базы эквивалентно переносу на уровне функций: отображение v+ᵥ b эквивалентно сложению v и b на уровне функций.

LaTeX

$$$\\text{coe}(v +ᵥ b) = \\text{coe}(v) + \\text{coe}(b)$$$

Lean4

@[simp, norm_cast]
theorem coe_vadd (v : V) (b : AffineBasis ι k P) : ⇑(v +ᵥ b) = v +ᵥ ⇑b :=
  rfl

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