instContinuousStarMatrix — Mathlib

English

If R has a star operation and a continuous star operation, then the star operation on M_{m×m}(R) is continuous.

Русский

Если у R есть операция звезды и она непрерывна, то операция звезды над матрицами M_{m×m}(R) непрерывна.

LaTeX

$$$\\operatorname{ContinuousStar}(\\mathrm{M}_{m\\times m}(R)).$$$

Lean4

instance [Star R] [ContinuousStar R] : ContinuousStar (Matrix m m R) :=
  ⟨continuous_id.matrix_conjTranspose⟩

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