Theorem Ideal.stdBasisMatrix_mem_jacobson_matricesOver

Modification history

2025-05-06 15:16

Mathlib/LinearAlgebra/Matrix/Ideal.lean

refactor: rename `Matrix.stdBasisMatrix` to `Matrix.single` (#24622) …

Deleted Ideal.stdBasisMatrix_mem_jacobson_matricesOver View on Github →

2024-11-07 19:30

Mathlib/LinearAlgebra/Matrix/Ideal.lean

feat(LinearAlgebra/Matrix): characterize Jacobson radicals in matrix rings (#17756)

Added Ideal.stdBasisMatrix_mem_jacobson_matricesOver View on Github →