norm_intCast_le_one

Mathlib.Analysis.Normed.Ring.Ultra

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.norm_intCast_le_one

English

The norm of any integer embedded in R is at most 1.

Русский

Норма целого числа, встроенного в R, не более 1.

LaTeX

$$$\| z : \mathbb{R} \| \le 1 \quad \text{for all } z \in \mathbb{Z}$$$

Lean4

theorem norm_intCast_le_one (z : ℤ) : ‖(z : R)‖ ≤ 1 :=
  nnnorm_intCast_le_one _ z

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

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

Разделы

Аффилиация

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