Theorems · Inductive type · ring theory
StarMemClass
(S : Type u_1) → (R : Type u_2) → [Star R] → [SetLike S R] → Prop
StarMemClass S G states S is a type of subsets s ⊆ G closed under star.
- Defined in
- Mathlib.Algebra.Star.Basic
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by30
Results whose statement or proof uses this declaration.
- StarMemClass.star_memstatement and proof · cited by 16
- NonUnitalStarSubalgebraClass.subtypestatement and proof · cited by 8
- StarMemClass.star_coe_eqstatement and proof · cited by 5
- NonUnitalStarSubalgebra.unitizationstatement and proof · cited by 4
- StarSubalgebra.ofClassstatement and proof · cited by 2
- NonUnitalStarSubalgebra.ofClassstatement and proof · cited by 2
- StarMemClass.coe_starstatement and proof · cited by 1
- NonUnitalStarSubalgebra.unitizationStarAlgEquivstatement and proof · cited by 1
- NonUnitalStarSubsemiring.ofClassstatement and proof · cited by 1
- StarSubalgebra.ofClass_carrierstatement and proof · cited by 1
- star_mem_iffstatement and proof · cited by 1
- StarSubsemiring.ofClassstatement and proof · cited by 1