English
There is a scalar action of a group G on AffineBasis ι k P given by (a • b)(i) = a • b(i), respecting the basis structure.
Русский
Существует действие скаляров группы G на AffineBasis ι k P: (a • b)(i) = a • b(i), сохраняющее структуру базиса.
LaTeX
$$$a \\cdot b\\;\\text{defined by } (a \\cdot b)(i) = a \\cdot b(i)$$$
Lean4
@[simp]
theorem coord_vadd (v : V) (b : AffineBasis ι k P) :
(v +ᵥ b).coord i = (b.coord i).comp (AffineEquiv.constVAdd k P v).symm :=
by
ext p
simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords, AffineMap.coe_mk,
AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap, Function.comp_apply,
AffineEquiv.constVAdd_apply, sub_right_inj]
congr! 1
rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]
