Commit 2024-10-04 04:46 a083bae2

View on Github →

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

Add a constructor TwoSidedIdeal.ofIdeal to turn an Ideal that happens to be two-sided into a TwoSidedIdeal.
Use ofIdeal to define a two-sided version of the Jacobson radical.
Generalize some ring lemmas that didn't need to assume commutativity.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ideal.mem_span_singleton_sup

Modified Mathlib/RingTheory/JacobsonIdeal.lean

added theorem Ideal.exists_mul_add_sub_mem_of_mem_jacobson

added theorem Ideal.jacobson_mul_mem_right

added theorem TwoSidedIdeal.asIdeal_jacobson

added def TwoSidedIdeal.jacobson

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

added theorem TwoSidedIdeal.coe_mk'

modified theorem TwoSidedIdeal.mem_mk'

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

added theorem Ideal.asIdeal_toTwoSided

added theorem Ideal.coe_toTwoSided

added theorem Ideal.mem_toTwoSided

added def Ideal.toTwoSided

added theorem Ideal.toTwoSided_asIdeal