y_mul_dvd

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For any n and any k ≥ 0, y_n(a) divides y_{n k}(a).

Русский

Для любых n и k y_n(a) делит y_{n k}(a).

LaTeX

$$$y^{(a)}_{n} \\mid y^{(a)}_{n k}$ for all k ∈ ℕ.$$

Lean4

theorem y_mul_dvd (n) : ∀ k, yn a1 n ∣ yn a1 (n * k)
  | 0 => dvd_zero _
  | k + 1 => by rw [Nat.mul_succ, yn_add]; exact dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

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

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

Разделы

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

Аффилиация

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