Theorem Ideal.toTwoSided_asIdeal

Modification history

2024-10-04 04:46

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

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

Added Ideal.toTwoSided_asIdeal View on Github →