Def Ideal.toTwoSided

Modification history

2024-10-04 04:46

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

feat(RingTheory): define two-sided Jacobson radical (#17341) …

Added Ideal.toTwoSided View on Github →