nnnorm_intCast_abs

Mathlib.Analysis.Normed.Ring.Basic

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

English

The NN-norm of (abs z).cast equals the NN-norm of z.cast.

Русский

NN-норма от (abs z).cast равна NN-норме z.cast.

LaTeX

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

Lean4

@[simp]
theorem nnnorm_intCast_abs (z : ℤ) : ‖((|z| : ℤ) : α)‖₊ = ‖(z : α)‖₊ := by simp [← nnnorm_natAbs]

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

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

Разделы

Аффилиация

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