Theorem TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital

Modification history

2024-10-01 14:00
Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals (#14460)
Added TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunitalView on Github →