fract — Mathlib

English

For any a in α, the fractional part of a is defined as fract(a) = a − ⌊a⌋, i.e., the part of a after the decimal point.

Русский

Для любого a ∈ α дробная часть дробь fract(a) определяется как fract(a) = a − ⌊a⌋, то есть часть числа после запятой.

LaTeX

$$$\operatorname{fract}(a) = a - \lfloor a \rfloor.$$$

Lean4

/-- `Int.fract a` the fractional part of `a`, is `a` minus its floor. -/
def fract (a : α) : α :=
  a - floor a

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