lean_workbook_plus_1519
ProvedProve that where is an integer and is a real number.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1519 (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := by sorry
Source
Prove that where is an integer and is a real number.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1519 (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := by sorry