convergent_of_zero

Mathlib.NumberTheory.DiophantineApproximation.Basic

URI: https://scilib.ai/kg/mathlib#Real.convergent_of_zero

← MathLib Explorer

English

All convergents of 0 are zero.

Русский

Все конвергенты нуля равны нулю.

LaTeX

$$$$\\forall n\\, (\\text{convergent } 0\, n)=0.$$$$

Lean4

/-- All convergents of `0` are zero. -/
@[simp]
theorem convergent_of_zero (n : ℕ) : convergent 0 n = 0 := by
  induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih => simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

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

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

Разделы

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

Аффилиация

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