Commit 2024-07-17 07:53 72690948

View on Github →

feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals (#14456)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

modified theorem TwoSidedIdeal.le_iff

added def TwoSidedIdeal.orderIsoRingCon

added theorem TwoSidedIdeal.ringCon_injective

added theorem TwoSidedIdeal.ringCon_le_iff

Created Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean

added theorem TwoSidedIdeal.bot_ringCon

added theorem TwoSidedIdeal.iInf_ringCon

added theorem TwoSidedIdeal.iSup_ringCon

added theorem TwoSidedIdeal.inf_ringCon

added theorem TwoSidedIdeal.mem_bot

added theorem TwoSidedIdeal.mem_iInf

added theorem TwoSidedIdeal.mem_inf

added theorem TwoSidedIdeal.mem_sInf

added theorem TwoSidedIdeal.mem_sup

added theorem TwoSidedIdeal.mem_sup_left

added theorem TwoSidedIdeal.mem_sup_right

added theorem TwoSidedIdeal.sInf_ringCon

added theorem TwoSidedIdeal.sSup_ringCon

added theorem TwoSidedIdeal.sup_ringCon

added theorem TwoSidedIdeal.top_ringCon