Structures · Data types
IsMulApply
IsMulApply 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 mul_apply
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- FunLike.coeMonoidHom
- FunLike.coeMulHom
- FunLike.coe_mul
- mul_apply
- FunLike.coe_coeMonoidHom
- FunLike.coeMonoidHom_injective
- FunLike.coe_coeMulHom
- IsMulApply.mul_apply
- prod_apply
- FunLike.coeMonoidHom_apply
- FunLike.commMonoid
- FunLike.isCancelMul
- FunLike.coe_coeMonoidHom'
- FunLike.rightCancelSemigroup
- FunLike.isLeftCancelMul
- FunLike.commGroup
- FunLike.monoid
- FunLike.mulOneClass
- FunLike.divInvOneMonoid
- SlashInvariantForm.coeHom_injective
- FunLike.coeMulHom_apply
- FunLike.coe_prod
- FunLike.isRightCancelMul
- FunLike.commSemigroup
- SlashInvariantForm.coeHom
- FunLike.cancelCommMonoid
- FunLike.rightCancelMonoid
- FunLike.leftCancelMonoid
- FunLike.divInvMonoid
- CuspForm.coeHom
- FunLike.coeMulHom_injective
- CuspForm.coeHom_apply
- ModularForm.coeHom
- FunLike.leftCancelSemigroup
- FunLike.semigroup
- FunLike.divisionMonoid
- FunLike.divisionCommMonoid
- ContinuousLinearMap.coe_mul'
- FunLike.group
- FunLike.cancelMonoid
Ancestors0
No ancestors.