fract_add_ofNat

Mathlib.Algebra.Order.Floor.Ring

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

English

For a ∈ R and n ∈ N with n ≥ 2, fract(a + n) = fract(a).

Русский

Пусть a ∈ R и n ∈ ℕ, n ≥ 2; fract(a + n) = fract(a).

LaTeX

$$$\forall a \in \mathbb{R}, \forall n \in \mathbb{N}, [n \ge 2] \Rightarrow \operatorname{fract}(a+n) = \operatorname{fract}(a)$$$

Lean4

@[simp]
theorem fract_add_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] : fract (a + ofNat(n)) = fract a :=
  fract_add_natCast a n

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

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

Разделы

Аффилиация

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