Commit 2024-10-01 14:00 26ad5cea

View on Github →

feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals (#14460)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Congruence/Basic.lean

added def RingCon.comap

Created Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean

added theorem TwoSidedIdeal.finsetProd_mem

added theorem TwoSidedIdeal.finsetSum_mem

added theorem TwoSidedIdeal.listProd_mem

added theorem TwoSidedIdeal.listSum_mem

added theorem TwoSidedIdeal.multiSetProd_mem

added theorem TwoSidedIdeal.multisetSum_mem

Created Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

added def TwoSidedIdeal.asIdeal

added def TwoSidedIdeal.asIdealOpposite

added theorem TwoSidedIdeal.coe_asIdeal

added def TwoSidedIdeal.comap

added def TwoSidedIdeal.fromIdeal

added theorem TwoSidedIdeal.gc

added def TwoSidedIdeal.ker

added def TwoSidedIdeal.map

added theorem TwoSidedIdeal.map_mono

added theorem TwoSidedIdeal.mem_asIdeal

added theorem TwoSidedIdeal.mem_asIdealOpposite

added theorem TwoSidedIdeal.mem_comap

added theorem TwoSidedIdeal.mem_fromIdeal

added theorem TwoSidedIdeal.mem_ker

added theorem TwoSidedIdeal.mem_span_iff

added theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure

added theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing

added theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital

added def TwoSidedIdeal.orderIsoIdeal

added theorem TwoSidedIdeal.set_mul_subset

added theorem TwoSidedIdeal.span_mono

added theorem TwoSidedIdeal.subset_mul_set

added theorem TwoSidedIdeal.subset_span