nnnorm_natAbs

Mathlib.Analysis.Normed.Ring.Basic

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

English

The NN-norm of natAbs of z in α equals the NN-norm of z cast into α.

Русский

NN-нормa от natAbs z в α равна NN-норме z cast в α.

LaTeX

$$$\mathrm{nnnorm}(z.natAbs.cast) = \mathrm{nnnorm}(z.cast).$$$

Lean4

theorem nnnorm_natAbs (z : ℤ) : ‖(z.natAbs : α)‖₊ = ‖(z : α)‖₊ := by
  simp [← NNReal.coe_inj, -Nat.cast_natAbs, norm_natAbs]

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

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

Разделы

Аффилиация

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