English
The Cartesian product G × G' acts on P × P' componentwise, making (G × G')-torsor structure on (P × P'). In particular, (v, v') + (p, p') = (v +ᵥ p, v' +ᵥ p').
Русский
Декартово произведение G × G' действует на P × P' по компонентам, образуя структуру торсора (G × G') на (P × P'). В частности, (v, v') + (p, p') = (v +ᵥ p, v' +ᵥ p').
LaTeX
$$$$ (v, v') + (p, p') = (v +ᵥ p,\, v' +ᵥ p') $$$$
Lean4
instance instAddTorsor : AddTorsor (G × G') (P × P')
where
vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)
zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)
vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2)
vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _)
vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _)
