instNormedStarGroup

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.instNormedStarGroup

English

There is a NormedStarGroup structure on Matrix m m α whenever α is a StarAddMonoid and NormedStarGroup.

Русский

Существует структура NormedStarGroup на Matrix m m α при условии, что α — StarAddMonoid и NormedStarGroup.

LaTeX

$$$\text{NormedStarGroup}(\text{Matrix } m\, m\, α).$$$

Lean4

instance [StarAddMonoid α] [NormedStarGroup α] : NormedStarGroup (Matrix m m α) :=
  ⟨(le_of_eq <| norm_conjTranspose ·)⟩

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

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

Разделы

Аффилиация

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