Structures · Algebra
StarMemClass
StarMemClass S G states S is a type of subsets s ⊆ G closed under star.
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- 2 explicit arguments · adds star_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- NonUnitalStarSubalgebra
- StarSubalgebra
- VonNeumannAlgebra
- StarSubsemiring
- NonUnitalStarSubsemiring
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- StarMemClass.star_mem
- NonUnitalStarSubalgebraClass.subtype
- StarMemClass.star_coe_eq
- NonUnitalStarSubalgebra.unitization
- StarSubalgebra.ofClass
- NonUnitalStarSubalgebra.ofClass
- NonUnitalStarSubalgebra.unitizationStarAlgEquiv
- StarSubsemiring.ofClass
- star_mem_iff
- NonUnitalStarSubalgebra.ofClass_carrier
- StarMemClass.coe_star
- NonUnitalStarSubsemiring.ofClass
- StarSubalgebra.ofClass_carrier
- NonUnitalStarSubalgebraClass.coe_subtype
- NonUnitalStarSubalgebra.unitization_injective
- mem_of_star_mem
- cfcₙ_mem
- StarMemClass.instStarModule
- NonUnitalStarSubalgebra.unitization.congr_simp
- NonUnitalStarSubsemiring.coe_ofClass
- NonUnitalStarSubalgebra.nonUnitalCStarAlgebra
- NonUnitalStarAlgebra.instIsMulCommutative_adjoin
- StarSubalgebra.ofClass.congr_simp
- StarMemClass.instStar
- NonUnitalStarSubalgebraClass.subtype_apply
- NonUnitalStarSubalgebra.unitization_apply
- StarMemClass.instStarRing
- NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra
- NonUnitalStarSubalgebra.ofClass.congr_simp
- StarSubalgebra.commCStarAlgebra
- StarSubsemiring.coe_ofClass
- StarMemClass.instStarAddMonoid
- cfc_mem
- NonUnitalStarSubalgebraClass.subtype_injective
- StarAlgebra.instIsMulCommutative_adjoin
- NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe
- NonUnitalStarSubalgebra.unitization_range
- StarSubalgebra.cstarAlgebra
- StarMemClass.instStarMul
- StarMemClass.instInvolutiveStar
Ancestors0
No ancestors.