yn_modEq_two

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For all n, yn(a, n) ≡ n (mod 2).

Русский

Для всех n: yn(a, n) ≡ n (mod 2).

LaTeX

$$$y^{(a)}_{n} \\equiv n \\pmod{2}$$$

Lean4

theorem yn_modEq_two : ∀ n, yn a1 n ≡ n [MOD 2]
  | 0 => by rfl
  | 1 => by simp [Nat.ModEq.refl]
  | n + 2 =>
    (yn_modEq_two n).add_right_cancel <|
      by
      rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))]
      exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

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

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

Разделы

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

Аффилиация

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