Structures · Algebra
StarModule
A star module A over a star ring R is a module which is a star additive monoid,
and the two star structures are compatible in the sense
star (r • a) = star r • star a.
Note that it is up to the user of this typeclass to enforce
[Semiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A], and that
the statement only requires [Star R] [Star A] [SMul R A].
If used as [CommRing R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A], this represents a
star algebra.
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- 2 explicit arguments · adds star_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances9
- Int
- Nat
- Real
- Rat
- NNReal
- NNRat
- Units
- Subtype
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by715
- StarSubalgebra.toSubalgebra
- realPart
- imaginaryPart
- NonUnitalStarAlgebra.adjoin
- StarAlgebra.adjoin
- StarModule.star_smul
- StarAlgebra.elemental
- StarSubalgebra.map
- StarSubalgebra.topologicalClosure
- NonUnitalStarAlgebra.elemental
- selfAdjoint.expUnitary
- StarAlgHom.ofId
- skewAdjointPart
- starL'
- Subalgebra.starClosure
- cfcₙAux
- QuasispectrumRestricts.nonUnitalStarAlgHom
- StarAlgebra.subset_adjoin
- SpectrumRestricts.starAlgHom
- StarSubalgebra.toNonUnitalStarSubalgebra
- StarAlgHom.range
- starLinearEquiv
- CStarModule.innerₛₗ
- realPart_add_I_smul_imaginaryPart
- starL
- StarSubalgebra.inclusion
- selfAdjointPart
- selfAdjoint.submodule
- realPart_apply_coe
- StarSubalgebra.centralizer
- Unitization.starMap
- StarSubalgebra.comap
- selfAdjoint.expUnitary_coe
- NonUnitalSubalgebra.starClosure
- skewAdjointPart_apply_coe
- Unitization.starLift
- IsSelfAdjoint.smul
- StarSubalgebra.subtype
- StarAlgebra.elemental.self_mem
- starₗᵢ
- StarAlgHom.ofId_apply
- imaginaryPart_apply_coe
- StarSubalgebra.topologicalClosure_minimal
- StarSubalgebra.le_topologicalClosure
- IsSelfAdjoint.coe_realPart
- IsSelfAdjoint.imaginaryPart
- SpectrumRestricts.cfcHom_eq_restrict
- NonUnitalStarSubalgebra.iSupLift
- StarSubalgebra.mem_toSubalgebra
- selfAdjointPart_apply_coe
Ancestors0
No ancestors.