Structures · Algebra
StarRing
A \-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
which is additive which makes `R` with its multiplicative structure into a \-multiplication
(i.e. star (r * s) = star s * star r).
- Defined in
- Mathlib.Algebra.Star.Basic
- Shape
- One type argument · adds star_add
Extends1
Extended by3
Concrete types that are instances32
- Int
- Nat
- Real
- Rat
- Complex
- NNReal
- ContinuousLinearMap
- BoundedContinuousFunction
- CStarMatrix
- NNRat
- TensorProduct
- Quaternion
- Unitization
- WithConv
- Matrix
- QuadraticAlgebra
- MeasureTheory.SimpleFunc
- DirectLimit
- DoubleCentralizer
- Zsqrtd
- ContinuousMapZero
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- ContinuousLinearMapWOT
- CliffordAlgebra
- FreeAlgebra
- CompactlySupportedContinuousMap
- Subtype
- Prod
- MulOpposite
- ContinuousMap
- LinearMap
How is a type an instance?
Loading the hierarchy index…
Assumed by1,924
- starRingEnd
- cfc
- cfcₙ
- CFC.sqrt
- Matrix.PosSemidef
- cfcHom
- Matrix.PosDef
- cfcₙHom
- StarSubalgebra.toSubalgebra
- NonUnitalStarAlgebra.adjoin
- CFC.abs
- IsSelfAdjoint.of_nonneg
- StarAlgebra.adjoin
- cfc_apply
- Matrix.unitaryGroup
- cfcₙ_apply
- cfcₙ_apply_of_not_predicate
- conjneg
- conj_trivial
- StarAlgebra.elemental
- cfcₙ_congr
- StarSubalgebra.map
- StarSubalgebra.topologicalClosure
- cfc_comp'
- cfc_id
- cfc_congr
- LE.le.isSelfAdjoint
- cfcₙ_id
- NonUnitalStarAlgebra.elemental
- selfAdjoint.expUnitary
- cfc_apply_of_not_predicate
- StarAlgHom.ofId
- star_mul_self_nonneg
- CFC.log
- cfc_id'
- CStarRing.norm_star_mul_self
- cfc.congr_simp
- cfcₙ_apply_of_not_map_zero
- starL'
- cfcₙ_eq_cfc
- IsSelfAdjoint.spectrumRestricts
- cfcHom_continuous
- CFC.conjSqrt
- cfc_const
- cfc_cases
- Subalgebra.starClosure
- NonUnitalStarSubalgebra.inclusion
- cfc_map_spectrum
- NonUnitalStarSubalgebra.centralizer
- cfcHom_id