one_le_nnnorm_one

Mathlib.Analysis.Normed.Ring.Basic

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

English

In a NormedRing β with Nontrivial β, 1 ≤ ||1||₊.

Русский

В нормированном кольце β не равном нулю, 1 ≤ ||1||₊.

LaTeX

$$$1 \leq \|1\|_{+}$$$

Lean4

theorem one_le_nnnorm_one (β) [NormedRing β] [Nontrivial β] : 1 ≤ ‖(1 : β)‖₊ :=
  one_le_norm_one β

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

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

Разделы

Аффилиация

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