norm_inr

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

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

English

Polar form for invertible first component holds: x = x.fst • exp 𝕜 (⅟x.fst • inr x.snd).

Русский

Полярная форма для обратимой первой компоненты: x = x.fst • exp 𝕜 (⅟x.fst • inr x.snd).

LaTeX

$$$x = x.fst \\cdot \\exp_{𝕜}(x.fst^{-1} \\cdot inr(x.snd))$$$

Lean4

@[simp]
theorem norm_inr (m : M) : ‖(inr m : tsze R M)‖ = ‖m‖ := by simp [norm_def]

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

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

Разделы

Аффилиация

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