Structures · Algebra
NonUnitalSemiring
An associative but not-necessarily unital semiring.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_assoc
Extends2
Extended by3
Concrete types that are instances33
- Nat
- SeparationQuotient
- Filter.Germ
- CStarMatrix
- TensorProduct
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- DomMulAct
- MeasureTheory.SimpleFunc
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DomAddAct
- SkewMonoidAlgebra
- PiTensorProduct
- ZeroAtInftyContinuousMap
- SetSemiring
- RingCon.Quotient
- CompactlySupportedContinuousMap
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- WithTop
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by444
- Matrix.mul_assoc
- NonUnitalStarAlgebra.adjoin
- IsSelfAdjoint.of_nonneg
- LE.le.isSelfAdjoint
- NonUnitalStarAlgebra.elemental
- Matrix.dotProduct_mulVec
- IsQuasiregular
- star_mul_self_nonneg
- Matrix.mulVec_mulVec
- Unitization.inrNonUnitalStarAlgHom
- Matrix.vecMul_vecMul
- NonUnitalStarSubalgebra.inclusion
- NonUnitalStarSubalgebra.topologicalClosure
- NonUnitalSubalgebra.centralizer
- NonUnitalStarSubalgebra.centralizer
- Finset.dvd_sum
- NonUnitalSubsemiring.centralizer
- Unitization.starMap
- LE.le.star_eq
- NonUnitalSubalgebra.starClosure
- NonUnitalSubalgebra.topologicalClosure
- Unitization.starLift
- NonUnitalStarSubalgebra.prod
- Unitization.unitsFstOne
- Unitization.inrNonUnitalAlgHom
- star_left_conjugate_nonneg
- star_left_conjugate_le_conjugate
- Unitization.lift
- star_le_star_iff
- NonUnitalStarSubalgebra.center
- IsStarProjection.nonneg
- NonUnitalAlgebra.elemental
- Unitization.inrNonUnitalStarAlgHom_apply
- NonUnitalSubsemiring.topologicalClosure
- mul_star_self_nonneg
- Unitization.unitsFstOne_mulEquiv_quasiregular
- NonUnitalStarSubalgebra.iSupLift
- star_lt_star_iff
- NonUnitalStarAlgebra.adjoin_le
- NonUnitalStarAlgebra.subset_adjoin
- NonUnitalAlgHom.toAlgHom
- NonUnitalAlgHom.toAlgHom_apply
- NonUnitalSubalgebra.toNonUnitalStarSubalgebra
- Matrix.star_mulVec
- IsSelfAdjoint.conjugate_le_conjugate
- NonUnitalAlgebra.adjoin_le_centralizer_centralizer
- Unitization.inrRangeEquiv
- Multiset.dvd_sum
- isQuasiregular_iff
- Unitization.inlRingHom