norm_inl

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

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

English

If R has a norm one class, then tsze R M inherits a NormOneClass structure.

Русский

Если в R существует класс нормы единицы, то tsze R M унаследует структуру NormOneClass.

LaTeX

$$$\\text{instance }[\\text{NormOneClass } R] \\Rightarrow \\text{NormOneClass}(\\mathrm{tsze}(R,M))$$$

Lean4

@[simp]
theorem norm_inl (r : R) : ‖(inl r : tsze R M)‖ = ‖r‖ := by simp [norm_def]

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

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

Разделы

Аффилиация

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