Theorems · Definition · ring theory
NonUnitalSubring.closure
{R : Type u} → [inst : NonUnitalNonAssocRing R] → Set R → NonUnitalSubring RThe NonUnitalSubring generated by a set.
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonUnitalNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- SetLike.coeproof · cited by 8,199
- Set.ofPredproof · cited by 6,101
- InfSet.sInfproof · cited by 935
- NonUnitalNonAssocRingstatement and proof · cited by 354
- NonUnitalSubringstatement and proof · cited by 185
Cited by25
Results whose statement or proof uses this declaration.
- NonUnitalSubring.subset_closurestatement · cited by 9
- NonUnitalSubring.closure_lestatement · cited by 7
- NonUnitalSubring.gistatement and proof · cited by 6
- NonUnitalSubring.closure_inductionstatement and proof · cited by 2
- NonUnitalSubring.closure_le_centralizer_centralizerstatement · cited by 1
- NonUnitalRingHom.eqOn_set_closurestatement and proof · cited by 1
- NonUnitalSubring.mem_closurestatement · cited by 1
- NonUnitalSubring.closure_eqstatement · cited by 1
- NonUnitalSubring.closure_monostatement · cited by 0
- NonUnitalSubring.closure_preimage_lestatement · cited by 0
- NonUnitalSubring.closure_sUnionstatement · cited by 0
- NonUnitalSubring.closure_unionstatement · cited by 0