Theorem TwoSidedIdeal.mem_jacobson_iff

Modification history

2024-11-07 19:30

Mathlib/RingTheory/JacobsonIdeal.lean

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

Added TwoSidedIdeal.mem_jacobson_iff View on Github →