English
There is a NormedSpace.Core structure on the complex scalar–vector space CStarMatrix(m,n,A) determined by the standard norm axioms: nonnegativity, compatibility with scalar multiplication, triangle inequality, and the norm–zero criterion.
Русский
Существуют базовые свойства нормированного пространства над ℂ на пространстве матриц CStarMatrix(m,n,A): неотрицательность нормы, совместимость с умножением на скаляры, треугольное неравенство, и норма равная нулю тогда и только тогда, когда матрица равна нулю.
LaTeX
$$$$\\|M\\| \\ge 0, \\quad \\|cM\\| = |c|\\|M\\|, \\quad \\|M_1 + M_2\\| \\le \\|M_1\\| + \\|M_2\\|, \\quad \\|M\\| = 0 \\iff M = 0.$$$$
Lean4
theorem normedSpaceCore : NormedSpace.Core ℂ (CStarMatrix m n A)
where
norm_nonneg M := (toCLM M).opNorm_nonneg
norm_smul c M := by rw [norm_def, norm_def, map_smul, norm_smul _ (toCLM M)]
norm_triangle M₁ M₂ := by simpa [← map_add] using norm_add_le (toCLM M₁) (toCLM M₂)
norm_eq_zero_iff := by simpa only [norm_def, norm_eq_zero, ← injective_iff_map_eq_zero'] using toCLM_injective
