English
Let G and G′ be additive groups acting on torsors P and P′ respectively. On the product P × P′ there is a natural coordinatewise action of G × G′; explicitly, for v ∈ G, v′ ∈ G′, p ∈ P, p′ ∈ P′, one has (v, v′) +ᵥ (p, p′) = (v +ᵥ p, v′ +ᵥ p′).
Русский
Пусть G и G′ — аддитивные группы, действующие на торсоры P и P′ соответственно. На произведении P × P′ имеется естественное покоординатное действие G × G′; то есть для v ∈ G, v′ ∈ G′, p ∈ P, p′ ∈ P′ выполняется (v, v′) +ᵥ (p, p′) = (v +ᵥ p, v′ +ᵥ p′).
LaTeX
$$$ (v, v') +^\\mathrm{v} (p, p') = (v +^\\mathrm{v} p, v' +^\\mathrm{v} p') $$$
Lean4
@[simp]
theorem mk_vadd_mk (v : G) (v' : G') (p : P) (p' : P') : (v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p') :=
rfl
