fract_nonneg

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.fract_nonneg

English

For every a, fract(a) ≥ 0.

Русский

Для любого a выполняется fract(a) ≥ 0.

LaTeX

$$0 \leq \operatorname{fract}(a)$$

Lean4

@[simp]
theorem fract_nonneg (a : R) : 0 ≤ fract a :=
  sub_nonneg.2 <| floor_le _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru