Commit 2024-11-07 19:30 af40115a

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

added theorem Ideal.matricesOver_jacobson_le

added theorem Ideal.stdBasisMatrix_mem_jacobson_matricesOver

added theorem TwoSidedIdeal.jacobson_matricesOver

added theorem TwoSidedIdeal.matricesOver_jacobson_bot

Modified Mathlib/RingTheory/JacobsonIdeal.lean

added theorem TwoSidedIdeal.mem_jacobson_iff

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean