floor_natCast

Mathlib.Algebra.Order.Floor.Ring

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

English

For every natural n, floor(n cast to R) equals n cast to R.

Русский

Для каждого натурального n: ⌊n в R⌋ = n в R.

LaTeX

$$$$ \\lfloor n \\cdot \\text{cast} \\rrbracket = n \\cdot \\text{cast} $$$$

Lean4

@[simp]
theorem floor_natCast (n : ℕ) : ⌊(n : R)⌋ = n :=
  eq_of_forall_le_iff fun a => by rw [le_floor, ← cast_natCast, cast_le]

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

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

Разделы

Аффилиация

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