Theorems · Theorem · ring theory
StarMemClass.star_mem
∀ {S : Type u_1} {R : Type u_2} {inst : Star R} {inst_1 : SetLike S R} [self : StarMemClass S R] {s : S} {r : R},
r ∈ s → star r ∈ sClosure under star.
- Defined in
- Mathlib.Algebra.Star.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- StarMemClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLikestatement and proof · cited by 1,084
- Star.starstatement · cited by 1,082
- Starstatement and proof · cited by 496
- StarMemClassstatement and proof · cited by 21
Cited by17
Results whose statement or proof uses this declaration.
- StarAlgebra.gcproof · cited by 4
- NonUnitalStarAlgebra.gcproof · cited by 3
- Subalgebra.SeparatesPoints.rclike_to_realproof · cited by 2
- StarAlgebra.adjoin_inductionstatement and proof · cited by 2
- NonUnitalStarSubalgebra.coe_iSup_of_directedproof · cited by 2
- NonUnitalSubalgebra.starClosure_leproof · cited by 2
- NonUnitalStarSubalgebra.ofClassproof · cited by 2
- Subalgebra.starClosure_leproof · cited by 1
- star_mem_iffproof · cited by 1
- NonUnitalStarAlgebra.star_self_mem_adjoin_singletonproof · cited by 1
- StarAlgebra.elemental.star_self_memproof · cited by 1
- NonUnitalStarAlgebra.adjoin_inductionstatement and proof · cited by 1