Commit 2024-07-05 15:27 d2e8846f

View on Github →

feat(RingTheory/TwosidedIdeal/Basic): define two-sided-ideal (#13902)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

added theorem TwoSidedIdeal.add_mem

added def TwoSidedIdeal.coeOrderEmbedding

added theorem TwoSidedIdeal.ext

added theorem TwoSidedIdeal.le_iff

added theorem TwoSidedIdeal.lt_iff

added theorem TwoSidedIdeal.mem_iff

added theorem TwoSidedIdeal.mem_mk'

added def TwoSidedIdeal.mk'

added theorem TwoSidedIdeal.mul_mem_left

added theorem TwoSidedIdeal.mul_mem_right

added theorem TwoSidedIdeal.neg_mem

added theorem TwoSidedIdeal.nsmul_mem

added theorem TwoSidedIdeal.rel_iff

added theorem TwoSidedIdeal.sub_mem

added theorem TwoSidedIdeal.zero_mem

added theorem TwoSidedIdeal.zsmul_mem

added structure TwoSidedIdeal