constVAdd_add — Mathlib

English

For v1, v2 ∈ G, constVAdd P (v1 + v2) = constVAdd P v1 · constVAdd P v2, i.e., constVAdd is a group homomorphism from G to permutations of P in multiplicative form.

Русский

Для v1, v2 ∈ G выполняется constVAdd P (v1 + v2) = constVAdd P v1 · constVAdd P v2, т.е. константная добавка образует гомоморфизм группы G в группы перестановок P.

LaTeX

$$$$ \text{constVAdd } P (v_1 + v_2) = \text{constVAdd } P v_1 \cdot \text{constVAdd } P v_2 $$$$

Lean4

@[simp]
theorem constVAdd_add (v₁ v₂ : G) : constVAdd P (v₁ + v₂) = constVAdd P v₁ * constVAdd P v₂ :=
  ext <| add_vadd v₁ v₂

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