Structures · Algebra
SubNegZeroMonoid
A SubNegMonoid where -0 = 0.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds neg_zero
Extends2
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances3
- EReal
- DomAddAct
- WithCStarModule
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- sub_zero
- zero_sub_zero
- Matrix.BlockTriangular.sub
- ProbabilityTheory.HasIndepIncrements.indepFun_eval_sub
- Matrix.diagonal_sub
- Finsupp.sub_apply
- Finsupp.mapRange_sub
- Finsupp.coe_sub
- SubNegZeroMonoid.neg_zero
- ContinuousMapZero.coe_sub
- SubNegZeroMonoid.toSubNegMonoid
- DomAddAct.instSubNegZeroMonoidOfAddOpposite
- WithCStarModule.instSubNegZeroMonoid
- TrivSqZeroExt.inl_sub
- ContinuousMapZero.instSub
- SubNegZeroMonoid.toNegZeroClass
- Function.Injective.subNegZeroMonoid
- Finsupp.instSub
- QuadraticAlgebra.C_sub
- TrivSqZeroExt.inr_sub
- Pi.subNegZeroMonoid
- FunLike.subNegZeroMonoid