y_mk

Mathlib.NumberTheory.Pell

URI: https://scilib.ai/kg/mathlib#Pell.Solution₁.y_mk

English

The y-coordinate of mk x y prop is exactly y.

Русский

Y-координата mk x y prop равна ровно y.

LaTeX

$$$$ (\mathrm{mk}(x,y,p)).y = y. $$$$

Lean4

@[simp]
theorem y_mk (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) : (mk x y prop).y = y :=
  rfl

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

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

Разделы

Аффилиация

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