Structures · Algebra
NegZeroClass
Typeclass for expressing that -0 = 0.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds neg_zero
Extends2
Extended by1
Concrete types that are instances4
- SeparationQuotient
- Filter.Germ
- DomAddAct
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by36
- neg_zero
- Function.Antiperiodic.nat_mul_eq_of_eq_zero
- Matrix.BlockTriangular.neg
- Matrix.diagonal_neg
- Function.Odd.map_zero
- HahnSeries.support_neg_subset
- Finsupp.mapRange_neg
- Finsupp.neg_apply
- NegZeroClass.neg_zero
- Finsupp.instNeg
- NegZeroClass.toNeg
- TrivSqZeroExt.inl_neg
- Pi.negZeroClass
- ZeroHom.instNeg
- ArithmeticFunction.instNeg
- Function.Odd.zero
- QuadraticAlgebra.C_neg
- ZeroHom.neg_comp
- ArithmeticFunction.neg_apply
- SeparationQuotient.instNegZeroClass
- Finsupp.coe_neg
- DomAddAct.instNegZeroClassOfAddOpposite
- ZeroHom.coe_neg
- FunLike.negZeroClass
- NegZeroClass.toZero
- HahnSeries.coeff_neg
- Function.Injective.negZeroClass
- Filter.Germ.instNegZeroClass
- TrivSqZeroExt.inr_neg
- ContinuousMapZero.instNeg
- HahnSeries.instNeg
- HahnSeries.coeff_neg'
- ContinuousMapZero.coe_neg
- HahnSeries.cardSupp_neg_le
- Matrix.single_neg
- ZeroHom.neg_apply