start_v

Mathlib.Data.PNat.Xgcd

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

← MathLib Explorer

English

The v-component of the start state is exactly the pair (a,b).

Русский

Компонента v начального состояния равна паре (a,b).

LaTeX

$$$\\text{start}(a,b).v = \\langle a, b \\rangle$$$

Lean4

theorem start_v (a b : ℕ+) : (start a b).v = ⟨a, b⟩ :=
  by
  dsimp [start, v, XgcdType.a, XgcdType.b, w, z]
  rw [one_mul, one_mul, zero_mul, zero_mul]
  have := a.pos
  have := b.pos
  congr <;> omega

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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