lean_workbook_plus_528
ProvedDenotes the fractional part, or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_528 (x : ℝ) : (Int.fract x) = x - Int.floor x := by sorry
Source
Denotes the fractional part, or .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_528 (x : ℝ) : (Int.fract x) = x - Int.floor x := by sorry