ysq_dvd_yy

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For a > 1 and n, y_n(a)^2 divides y_{n·y_n(a)}(a).

Русский

Для a > 1 и n верно y_n(a)^2 делит y_{n·y_n(a)}(a).

LaTeX

$$$y^{(a)}_{n}{}^{2} \\mid y^{(a)}_{n\\cdot y^{(a)}_{n}}$$$

Lean4

theorem ysq_dvd_yy (n) : yn a1 n * yn a1 n ∣ yn a1 (n * yn a1 n) :=
  modEq_zero_iff_dvd.1 <|
    ((xy_modEq_yn a1 n (yn a1 n)).right.of_dvd <| by simp [_root_.pow_succ]).trans
      (modEq_zero_iff_dvd.2 <| by simp [mul_dvd_mul_left, mul_assoc])

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

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

Разделы

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

Аффилиация

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