coe_constVAdd

Mathlib.Algebra.AddTorsor.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.coe_constVAdd

English

The map v ↦ v +ᵥ p defines a permutation of P for fixed p ∈ P.

Русский

Отображение v ↦ v +ᵥ p задаёт перестановку множества P для фиксированного p.

LaTeX

$$$\mathrm{vaddConst}(p): G \to P,\quad v \mapsto v +ᵥ p$ is a bijection with inverse $p' \mapsto p' -ᵥ p$$$

Lean4

@[simp]
theorem coe_constVAdd (v : G) : ⇑(constVAdd P v) = (v +ᵥ ·) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru