v_eq_succ_vp

Mathlib.Data.PNat.Xgcd

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

English

For any state u, the vector v equals the coordinate-wise successor of vp: v = succ₂(vp).

Русский

Для любого состояния v равен по координатному применению succ₂ к vp: v = succ₂(vp).

LaTeX

$$$v = \\text{succ}_2(\\,vp\\,)$$$

Lean4

theorem v_eq_succ_vp : u.v = succ₂ u.vp := by ext <;> dsimp [v, vp, w, z, a, b, succ₂] <;> ring_nf

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

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

Разделы

Аффилиация

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