Commit 2025-05-06 15:16 e214b5b0

refactor: rename Matrix.stdBasisMatrix to Matrix.single (#24622) This also moves things out of the Matrix.StdBasisMatrix namespace, which didn't follow the naming guide. The new name is in sync with Wikipedia's name for this construct, a "single-entry matrix", and also matches Pi.single, (D)Finsupp.single, and (Add)MonoidAlgebra.single. Deprecations were added with the deprecations script, and then the namespaces adjusted manually. Zulip thread: #mathlib4 > Renaming docs#Matrix.stdBasisMatrix @ 💬 Moves:

• Matrix.stdBasisMatrix → Matrix.single
• Matrix.stdBasisMatrix_eq_of_single_single → Matrix.single_eq_of_single_single
• Matrix.of_symm_stdBasisMatrix → Matrix.of_symm_single
• Matrix.smul_stdBasisMatrix → Matrix.smul_single
• Matrix.stdBasisMatrix_zero → Matrix.single_zero
• Matrix.transpose_stdBasisMatrix → Matrix.transpose_single
• Matrix.map_stdBasisMatrix → Matrix.map_single
• Matrix.stdBasisMatrix_add → Matrix.single_add
• Matrix.mulVec_stdBasisMatrix → Matrix.single_mulVec
• Matrix.matrix_eq_sum_stdBasisMatrix → Matrix.matrix_eq_sum_single
• Matrix.stdBasisMatrix_eq_single_vecMulVec_single → Matrix.single_eq_single_vecMulVec_single
• Matrix.stdBasisMatrixAddMonoidHom → Matrix.singleAddMonoidHom
• Matrix.stdBasisMatrixLinearMap → Matrix.singleLinearMap
• Matrix.StdBasisMatrix.apply_same → Matrix.single_apply_same
• Matrix.StdBasisMatrix.apply_of_ne → Matrix.single_apply_of_ne
• Matrix.StdBasisMatrix.apply_of_row_ne → Matrix.single_apply_of_row_ne
• Matrix.StdBasisMatrix.apply_of_col_ne → Matrix.single_apply_of_col_ne
• Matrix.StdBasisMatrix.diag_zero → Matrix.diag_single_of_ne
• Matrix.StdBasisMatrix.diag_same → Matrix.diag_single_same
• Matrix.StdBasisMatrix.mul_left_apply_same → Matrix.single_mul_apply_same
• Matrix.StdBasisMatrix.mul_right_apply_same → Matrix.mul_single_apply_same
• Matrix.StdBasisMatrix.mul_left_apply_of_ne → Matrix.single_mul_apply_of_ne
• Matrix.StdBasisMatrix.mul_right_apply_of_ne → Matrix.mul_single_apply_of_ne
• Matrix.StdBasisMatrix.mul_same → Matrix.single_mul_single_same
• Matrix.stdBasisMatrix_mul_mul_stdBasisMatrix → Matrix.single_mul_mul_single
• Matrix.StdBasisMatrix.mul_of_ne → Matrix.single_mul_single_of_ne
• Matrix.row_eq_zero_of_commute_stdBasisMatrix → Matrix.row_eq_zero_of_commute_single
• Matrix.col_eq_zero_of_commute_stdBasisMatrix → Matrix.col_eq_zero_of_commute_single
• Matrix.diag_eq_of_commute_stdBasisMatrix → Matrix.diag_eq_of_commute_single
• Matrix.mem_range_scalar_of_commute_stdBasisMatrix → Matrix.mem_range_scalar_of_commute_single
• Matrix.mem_range_scalar_iff_commute_stdBasisMatrix → Matrix.mem_range_scalar_iff_commute_single
• Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' → Matrix.mem_range_scalar_iff_commute_single'
• Matrix.comp_stdBasisMatrix_stdBasisMatrix → Matrix.comp_single_single
• Matrix.comp_symm_stdBasisMatrix → Matrix.comp_symm_single
• Matrix.conjTranspose_stdBasisMatrix → Matrix.conjTranspose_single
• Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_eq → Matrix.single_hadamard_single_eq
• Matrix.kroneckerMap_stdBasisMatrix_stdBasisMatrix → Matrix.kroneckerMap_single_single
• Matrix.stdBasisMatrix_kronecker_stdBasisMatrix → Matrix.single_kronecker_single
• Matrix.stdBasisMatrix_kroneckerTMul_stdBasisMatrix → Matrix.single_kroneckerTMul_single
• Matrix.blockTriangular_stdBasisMatrix → Matrix.blockTriangular_single
• Matrix.blockTriangular_stdBasisMatrix' → Matrix.blockTriangular_single'
• Ideal.stdBasisMatrix_mem_jacobson_matricesOver → Ideal.single_mem_jacobson_matricesOver
• RingCon.matrix_apply_stdBasisMatrix → RingCon.matrix_apply_single
• Matrix.stdBasis_eq_stdBasisMatrix → Matrix.stdBasis_eq_single
• Matrix.StdBasisMatrix.trace_zero → Matrix.trace_single_eq_of_ne
• Matrix.StdBasisMatrix.trace_eq → Matrix.trace_single_eq_same
• kroneckerTMulAlgEquiv_symm_stdBasisMatrix_tmul → kroneckerTMulAlgEquiv_symm_single_tmul
• matrixEquivTensor_apply_stdBasisMatrix → matrixEquivTensor_apply_single