norm_inv

Mathlib.Analysis.Normed.Field.Basic

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

English

The norm of an inverse equals the reciprocal of the norm: ||a^{-1}|| = ||a||^{-1}.

Русский

Норма обратного элемента равна обратной нормы: ||a^{-1}|| = ||a||^{-1}.

LaTeX

$$$\\|a^{-1}\\| = \\|a\\|^{-1}$$$

Lean4

@[simp]
theorem norm_inv (a : α) : ‖a⁻¹‖ = ‖a‖⁻¹ :=
  map_inv₀ (normHom : α →*₀ ℝ) a

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

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

Разделы

Аффилиация

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