term_†

Mathlib.Analysis.InnerProductSpace.Adjoint

URI: https://scilib.ai/kg/mathlib#InnerProduct.term_†

← MathLib Explorer

English

The norm of adjointAux A equals the norm of A: ||adjointAux A|| = ||A||.

Русский

Норма adjointAux A равна норме A: ||adjointAux A|| = ||A||.

LaTeX

$$$$ \\| \\mathrm{adjointAux} A \\| = \\| A \\|. $$$$

Lean4

@[inherit_doc ContinuousLinearMap.adjoint, scoped term_parser 1000]
public meta def «term_†» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `InnerProduct.«term_†» 1000 1000 (ParserDescr.symbol✝ "†")

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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