start_isSpecial

Mathlib.Data.PNat.Xgcd

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

English

The initial state produced by start on positive naturals is special: (start a b).IsSpecial.

Русский

Начальное состояние, получаемое функцией start на положительных натуральных числах, является специальным: (start a b).IsSpecial.

LaTeX

$$$\\text{IsSpecial}(\\text{start}(a,b))$$$

Lean4

theorem start_isSpecial (a b : ℕ+) : (start a b).IsSpecial := by dsimp [start, IsSpecial]

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

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

Разделы

Аффилиация

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