Structures · Data types
IsNegApply
IsNegApply F α β states for all f : F and x : α, (-f) x = -f x.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 3 explicit arguments · adds neg_apply
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances12
- ContinuousLinearMap
- ContinuousMultilinearMap
- SchwartzMap
- MeasureTheory.VectorMeasure
- TestFunction
- ContDiffMapSupportedIn
- UniformConvergenceCLM
- ModularForm
- SlashInvariantForm
- CuspForm
- QuadraticMap
- MultilinearMap
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- neg_apply
- FunLike.coe_neg
- IsNegApply.neg_apply
- QuadraticMap.coeFn_neg
- FunLike.subNegMonoid
- SlashInvariantForm.coe_neg
- FunLike.addCommGroup
- MeasureTheory.VectorMeasure.coe_neg
- FunLike.subtractionCommMonoid
- ContinuousLinearMap.coe_neg'
- FunLike.addGroup
- ContDiffMapSupportedIn.coe_neg
- MeasureTheory.VectorMeasure.neg_apply
- ModularForm.neg_apply
- ModularForm.coe_neg
- SlashInvariantForm.neg_apply
- ContinuousLinearMap.neg_apply
- FunLike.involutiveNeg
- UniformConvergenceCLM.neg_apply
- TestFunction.coe_neg
- FunLike.ring
- QuadraticMap.neg_apply
- FunLike.subtractionMonoid
- MultilinearMap.neg_apply
- FunLike.negZeroClass
- CuspForm.neg_apply
- ContinuousMultilinearMap.neg_apply
- CuspForm.coe_neg
- FunLike.subNegZeroMonoid
- SchwartzMap.neg_apply
Ancestors0
No ancestors.