prop_x

Mathlib.NumberTheory.Pell

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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