xn_one

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.xn_one

English

The x-coordinate after one step equals a: x_1 = a.

Русский

После одного шага x-координата равна a: x_1 = a.

LaTeX

$$$x_1 = a.$$$

Lean4

theorem xn_one : xn a1 1 = a := by simp

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

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

Разделы

Аффилиация

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