Commit 2023-06-22 00:17 e53fb911

View on Github →

feat: port Analysis.Matrix (#4490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Matrix.lean

added def Matrix.frobeniusNormedAddCommGroup

added def Matrix.frobeniusNormedAlgebra

added def Matrix.frobeniusNormedRing

added def Matrix.frobeniusNormedSpace

added def Matrix.frobeniusSeminormedAddCommGroup

added theorem Matrix.frobenius_nnnorm_col

added theorem Matrix.frobenius_nnnorm_conjTranspose

added theorem Matrix.frobenius_nnnorm_def

added theorem Matrix.frobenius_nnnorm_diagonal

added theorem Matrix.frobenius_nnnorm_map_eq

added theorem Matrix.frobenius_nnnorm_mul

added theorem Matrix.frobenius_nnnorm_one

added theorem Matrix.frobenius_nnnorm_row

added theorem Matrix.frobenius_nnnorm_transpose

added theorem Matrix.frobenius_norm_col

added theorem Matrix.frobenius_norm_conjTranspose

added theorem Matrix.frobenius_norm_def

added theorem Matrix.frobenius_norm_diagonal

added theorem Matrix.frobenius_norm_map_eq

added theorem Matrix.frobenius_norm_mul

added theorem Matrix.frobenius_norm_row

added theorem Matrix.frobenius_norm_transpose

added theorem Matrix.linfty_op_nnnorm_col

added theorem Matrix.linfty_op_nnnorm_def

added theorem Matrix.linfty_op_nnnorm_diagonal

added theorem Matrix.linfty_op_nnnorm_mul

added theorem Matrix.linfty_op_nnnorm_mulVec

added theorem Matrix.linfty_op_nnnorm_row

added theorem Matrix.linfty_op_norm_col

added theorem Matrix.linfty_op_norm_def

added theorem Matrix.linfty_op_norm_diagonal

added theorem Matrix.linfty_op_norm_mul

added theorem Matrix.linfty_op_norm_mulVec

added theorem Matrix.linfty_op_norm_row

added theorem Matrix.nnnorm_col

added theorem Matrix.nnnorm_conjTranspose

added theorem Matrix.nnnorm_def

added theorem Matrix.nnnorm_diagonal

added theorem Matrix.nnnorm_entry_le_entrywise_sup_nnnorm

added theorem Matrix.nnnorm_le_iff

added theorem Matrix.nnnorm_lt_iff

added theorem Matrix.nnnorm_map_eq

added theorem Matrix.nnnorm_row

added theorem Matrix.nnnorm_transpose

added theorem Matrix.norm_col

added theorem Matrix.norm_conjTranspose

added theorem Matrix.norm_def

added theorem Matrix.norm_diagonal

added theorem Matrix.norm_entry_le_entrywise_sup_norm

added theorem Matrix.norm_le_iff

added theorem Matrix.norm_lt_iff

added theorem Matrix.norm_map_eq

added theorem Matrix.norm_row

added theorem Matrix.norm_transpose

Modified Mathlib/Data/Matrix/Basic.lean