lean_workbook_plus_25310

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find $\lim_{n \to \infty} \left\{(a + b\sqrt {c})^n\right\}$ given $a = 1 + [b\sqrt c]$ and $\sqrt c \not\in \mathbb{Q}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25310 (a b c : ℝ) (h₁ : a = 1 + b * Real.sqrt c) (h₂ : Real.sqrt c ∉ Set.range ((↑) : ℚ → ℝ)) : ∃ n : ℕ, ∀ ε : ℝ, ε > 0 → |(a + b * Real.sqrt c)^n - 1| < ε   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph