Structures · Lean core
Neg
The notation typeclass for negation.
This enables the notation -a : α where a : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds neg
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Concrete types that are instances100
- Int
- Real
- Rat
- Bool
- Quiver.Hom
- Complex
- SeparationQuotient
- BitVec
- ContinuousLinearMap
- Polynomial
- Filter.Germ
- BoundedContinuousFunction
- Padic
- CStarMatrix
- RatFunc
- UniformSpace.Completion
- UInt64
- TensorProduct
- UInt8
- UInt16
- UInt32
- Unitization
- Matrix
- WithVal
- HahnSeries
- NonemptyInterval
- LocallyConstant
- USize
- QuadraticAlgebra
- Units
- MeasureTheory.SimpleFunc
- EReal
- RestrictedProduct
- TrivSqZeroExt
- Finsupp
- UniformFun
- DoubleCentralizer
- Zsqrtd
- UniformOnFun
- ZNum
- SymAlg
- DomAddAct
- SkewMonoidAlgebra
- Interval
- AddUnits
- ContinuousMapZero
- CauSeq.Completion.Cauchy
- PerfectClosure
- OreLocalization
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- Int32
- Int8
- Int64
- ContinuousAlternatingMap
- Int16
- DFinsupp
- WittVector
- CauSeq
- TruncatedWittVector
- WithCStarModule
- ArithmeticFunction
- AdicCompletion
- Matrix.SpecialLinearGroup
- MeasureTheory.AEEqFun
- ISize
- Representation.IntertwiningMap
- AdicCompletion.AdicCauchySequence
- RingCon.Quotient
- HomogeneousLocalization
- RingQuot
- CentroidHom
- CommRingCat.Colimits.ColimitType
- Poly
- SignType
- ContinuousMultilinearMap
- CompactlySupportedContinuousMap
- SchwartzMap
- FreeAddGroup
- MeasureTheory.VectorMeasure
- Hamming
- AlternatingMap
- IncidenceAlgebra
- AddMonoidHom
- ContinuousAffineMap
- ArchimedeanClass
- RingCat.Colimits.ColimitType
- DMatrix
- NormedAddGroupHom
- ZeroHom
- TestFunction
- ContDiffMapSupportedIn
- Function.locallyFinsuppWithin
- Derivation
- AffineMap
- Part
- LieDerivation
- LeftInvariantDerivation
- ModularForm
- SlashInvariantForm
How is a type an instance?
Loading the hierarchy index…
Assumed by427
- Quaternion
- Set.neg
- SignType.cast
- Function.Antiperiodic
- Finset.neg
- castZNum
- Function.Odd
- Function.Even
- Filter.Tendsto.neg
- Set.mem_neg
- Continuous.fun_neg
- Pi.neg_apply
- SummationFilter.symmetricIco
- MeasureTheory.lconvolution
- SummationFilter.symmetricIcc
- List.alternatingSum
- MeasureTheory.Measure.neg
- ContinuousOn.neg
- ContinuousOn.fun_neg
- FunLike.coe_neg
- Set.inter_neg
- MeasureTheory.AEStronglyMeasurable.neg
- Continuous.neg
- Measurable.neg
- MeasureTheory.StronglyMeasurable.neg
- ContinuousWithinAt.neg
- MeasureTheory.Measure.map_neg_eq_self
- Measurable.fun_neg
- AEMeasurable.neg
- Set.neg_preimage
- ContinuousAt.neg
- Finset.zsmul
- Matrix.neg_cons
- Matrix.neg_empty
- MeasureTheory.Measure.measurePreserving_neg
- ZNum.cast_pos
- Filter.EventuallyEq.neg
- ZNum.cast_neg
- Pi.neg_def
- FirstOrder.Ring.realize_zero
- Quaternion.equivProd
- Set.ZSMul
- Function.Antiperiodic.sub_eq'
- ContinuousAt.fun_neg
- TrivSqZeroExt.fst_inv
- MeasureTheory.SimpleFunc.negPart
- Unitization.inr_neg
- Function.Periodic.add_antiperiod_eq
- Finset.neg_nonempty_iff
- SignType.coe_one
Ancestors0
No ancestors.