floor_real_sqrt_eq_nat_sqrt — Mathlib

English

For every a ∈ ℕ, ⌊√(a)⌋ = Nat.sqrt a.

Русский

Для любого a ∈ ℕ выполняется ⌊√(a)⌋ = Nat.sqrt a.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{N}, \\\\lfloor \\\\sqrt{(a \\\\in \\\\mathbb{R})} \\\\rfloor = \\\\operatorname{Nat}.sqrt a$$$

Lean4

/-- The floor of the real square root is the same as the natural square root. -/
@[simp]
theorem floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋ = Nat.sqrt a :=
  by
  rw [Int.floor_eq_iff]
  exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

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