prop_y

Mathlib.NumberTheory.Pell

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

← MathLib Explorer

English

For any a ∈ Pell.Solution₁ d, d a.y^2 = a.x^2 - 1.

Русский

Для любого a ∈ Pell.Solution₁ d выполняется d a.y^2 = a.x^2 - 1.

LaTeX

$$$$ d \; a.y^2 = a.x^2 - 1. $$$$

Lean4

/-- An alternative form of the equation, suitable for rewriting `d * y^2`. -/
theorem prop_y (a : Solution₁ d) : d * a.y ^ 2 = a.x ^ 2 - 1 := by rw [← a.prop]; ring

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

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

Разделы

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

Аффилиация

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