round_ofNat

Mathlib.Algebra.Order.Round

URI: https://scilib.ai/kg/mathlib#round_ofNat

English

For n ≥ 2, rounding of ofNat(n) (the natural embedding into α) equals ofNat(n): round(ofNat(n)) = ofNat(n).

Русский

Для n ≥ 2 округление ofNat(n) (естественного в α) равно ofNat(n): round(ofNat(n)) = ofNat(n).

LaTeX

$$$\operatorname{round}(\operatorname{ofNat}(n)) = \operatorname{ofNat}(n) \quad (n \ge 2)$$$

Lean4

@[simp]
theorem round_ofNat (n : ℕ) [n.AtLeastTwo] : round (ofNat(n) : α) = ofNat(n) :=
  round_natCast n

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

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

Разделы

Аффилиация

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