Structures · Data types
IsSubApply
IsSubApply F α β states for all f g : F and x : α, (f - g) x = f x - g x.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 3 explicit arguments · adds sub_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 by28
- sub_apply
- FunLike.coe_sub
- IsSubApply.sub_apply
- SlashInvariantForm.coe_sub
- ModularForm.coe_sub
- FunLike.subNegMonoid
- FunLike.addCommGroup
- ContDiffMapSupportedIn.coe_sub
- QuadraticMap.coeFn_sub
- FunLike.subtractionCommMonoid
- FunLike.addGroup
- UniformConvergenceCLM.sub_apply
- ContinuousLinearMap.coe_sub'
- MeasureTheory.VectorMeasure.coe_sub
- CuspForm.coe_sub
- MultilinearMap.sub_apply
- FunLike.ring
- ContinuousLinearMap.sub_apply
- FunLike.subtractionMonoid
- MeasureTheory.VectorMeasure.sub_apply
- SchwartzMap.sub_apply
- TestFunction.coe_sub
- SlashInvariantForm.sub_apply
- QuadraticMap.sub_apply
- ModularForm.sub_apply
- ContinuousMultilinearMap.sub_apply
- FunLike.subNegZeroMonoid
- CuspForm.sub_apply
Ancestors0
No ancestors.