flip_v

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.flip_v

English

Under flip, the v-vector is the swap of the original: (flip u).v = u.v.swap.

Русский

При flip вектор v становится обменом исходного: (flip u).v = u.v.swap.

LaTeX

$$$(flip\\,u).v = u.v.swap$$$

Lean4

theorem flip_v : (flip u).v = u.v.swap := by
  dsimp [v]
  ext
  · simp only
    ring
  · simp only
    ring

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

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

Разделы

Аффилиация

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