Structures · Algebra
StarAddMonoid
A \*-additive monoid R is an additive monoid with an involutive star operation which
preserves addition.
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- One type argument · adds star_add
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances16
- BoundedContinuousFunction
- CStarMatrix
- TensorProduct
- Unitization
- WithConv
- Matrix
- MeasureTheory.SimpleFunc
- DirectLimit
- DoubleCentralizer
- ZeroAtInftyContinuousMap
- CentroidHom
- CompactlySupportedContinuousMap
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by396
- selfAdjoint
- star_zero
- realPart
- imaginaryPart
- skewAdjoint
- StarAddMonoid.star_add
- starAddEquiv
- norm_star
- skewAdjointPart
- starL'
- Unitization.inrNonUnitalStarAlgHom
- IsSelfAdjoint.sub
- star_sub
- starLinearEquiv
- realPart_add_I_smul_imaginaryPart
- star_sum
- starL
- selfAdjointPart
- selfAdjoint.submodule
- realPart_apply_coe
- Matrix.conjTransposeAddEquiv
- star_neg
- IsSelfAdjoint.add
- skewAdjointPart_apply_coe
- BoundedContinuousFunction.toContinuousMapStarₐ
- IsSelfAdjoint.neg
- starₗᵢ
- imaginaryPart_apply_coe
- IsSelfAdjoint.coe_realPart
- Unitization.inrNonUnitalStarAlgHom_apply
- star_isometry
- IsSelfAdjoint.imaginaryPart
- selfAdjointPart_apply_coe
- skewAdjoint.negISMul_apply_coe
- selfAdjoint.star_val_eq
- starAddEquiv_apply
- Unitization.isSelfAdjoint_inr
- realPart_I_smul
- StarModule.decomposeProdAdjoint
- skewAdjoint.submodule
- HasFDerivAtFilter.star
- Unitization.inrRangeEquiv
- skewAdjoint.mem_iff
- nnnorm_star
- HasDerivAtFilter.star
- Unitization.isStarNormal_inr
- Matrix.kroneckerTMulStarAlgEquiv
- HasDerivAt.star_conj
- Matrix.IsHermitian.sub
- Unitization.inr_star