Theorems · Theorem · ring theory
TwoSidedIdeal.mem_span_iff
∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s : Set R} {x : R},
x ∈ TwoSidedIdeal.span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I- Cited by
- 6 results in Mathlib
- Foundations
- Depth 43 from the axioms · uses propext, Quot.sound
- Assumes
- NonUnitalNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- SetLike.coestatement and proof · cited by 8,199
- Set.ofPredproof · cited by 6,101
- InfSet.sInfproof · cited by 935
- NonUnitalNonAssocRingstatement and proof · cited by 354
- SetLike.mem_coeproof · cited by 302
- RingConproof · cited by 219
- TwoSidedIdealstatement and proof · cited by 151
- sInf_leproof · cited by 110
- TwoSidedIdeal.spanstatement and proof · cited by 9
- TwoSidedIdeal.rel_iffproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- TwoSidedIdeal.span_monoproof · cited by 3
- TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbingproof · cited by 2
- TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunitalproof · cited by 0
- TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closureproof · cited by 0
- TwoSidedIdeal.gcproof · cited by 0
- TwoSidedIdeal.span_inductionproof · cited by 0