Structures · Data types
IsMulApplyEqComp
IsMulApplyEqComp F α α states for all x : α, (f * g) x = f (g x).
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 2 explicit arguments · adds mul_apply_eq_comp
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- ContinuousLinearMap
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by10
Ancestors0
No ancestors.