nnnorm_inr

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.nnnorm_inr

English

The nnnorm of inr m equals the nnnorm of m.

Русский

N(nnNorm) inr m равна nnnorm m.

LaTeX

$$$\\|\\mathrm{inr}(m)\\|_{nn} = \\|m\\|_{nn}$$$

Lean4

@[simp]
theorem nnnorm_inr (m : M) : ‖(inr m : tsze R M)‖₊ = ‖m‖₊ := by simp [nnnorm_def]

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

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

Разделы

Аффилиация

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