English
An auxiliary normed additively commutative group on matrices is constructed via an induced structure from Euclidean linear maps, yielding a canonical L2-operator norm.
Русский
Вводится вспомогательная структура нормированной аддитивно-коммутативной группы на матрицах путем индукции из линейных отображений Евклидова пространства, образуя норму L2-оператора.
LaTeX
$$$l2OpNormedAddCommGroupAux : NormedAddCommGroup (Matrix m n 𝕜)$$$
Lean4
/-- An auxiliary definition used only to construct the true `NormedAddCommGroup` (and `Metric`)
structure provided by `Matrix.instMetricSpaceL2Op` and `Matrix.instNormedAddCommGroupL2Op`. -/
def l2OpNormedAddCommGroupAux : NormedAddCommGroup (Matrix m n 𝕜) :=
@NormedAddCommGroup.induced ((Matrix m n 𝕜) ≃ₗ[𝕜] (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)) _ _ _ _
ContinuousLinearMap.toNormedAddCommGroup.toNormedAddGroup _ _ <|
(toEuclideanLin.trans toContinuousLinearMap).injective
