Structures · Data types
IsOneApply
IsOneApply F α β states for all x : α, (1 : F) x = 1.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 3 explicit arguments · adds one_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 by30
- FunLike.coeMonoidHom
- one_apply
- FunLike.coe_one
- FunLike.coe_coeMonoidHom
- FunLike.coeMonoidHom_injective
- IsOneApply.one_apply
- prod_apply
- FunLike.coeMonoidHom_apply
- FunLike.commMonoid
- FunLike.coe_coeMonoidHom'
- FunLike.commGroup
- FunLike.monoid
- FunLike.coe_one_iff
- FunLike.mulOneClass
- FunLike.divInvOneMonoid
- FunLike.invOneClass
- SlashInvariantForm.coeHom_injective
- FunLike.coe_prod
- SlashInvariantForm.coeHom
- FunLike.cancelCommMonoid
- FunLike.rightCancelMonoid
- FunLike.leftCancelMonoid
- FunLike.divInvMonoid
- CuspForm.coeHom
- CuspForm.coeHom_apply
- ModularForm.coeHom
- FunLike.divisionMonoid
- FunLike.divisionCommMonoid
- FunLike.group
- FunLike.cancelMonoid
Ancestors0
No ancestors.