norm_eq_one

Mathlib.Analysis.Normed.Ring.Finite

URI: https://scilib.ai/kg/mathlib#IsOfFinOrder.norm_eq_one

English

If a ∈ α has finite order (IsOfFinOrder a), then its norm is 1: ||a|| = 1.

Русский

Если элемент a имеет конечный порядок (IsOfFinOrder a), то его норма равна единице: ||a|| = 1.

LaTeX

$$$\|a\| = 1 \quad\text{при } \text{IsOfFinOrder } a$$$

Lean4

protected theorem norm_eq_one (ha : IsOfFinOrder a) : ‖a‖ = 1 :=
  ((normHom : α →*₀ ℝ).toMonoidHom.isOfFinOrder ha).eq_one <| norm_nonneg _

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

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

Разделы

Аффилиация

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