Structures · Data types
IsOneApplyEqSelf
IsOneApplyEqSelf F α α states for all x : α, (1 : F) x = x.
- Defined in
- Mathlib.Data.FunLike.IsApply
- Shape
- 2 explicit arguments · adds one_apply_eq_self
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 by15
- one_apply_eq_self
- FunLike.coe_one_eq_id
- FunLike.coe_pow_eq_iterate
- FunLike.natCast_eq_nsmul_one
- IsOneApplyEqSelf.one_apply_eq_self
- FunLike.intCast_eq_zsmul_one
- pow_apply_eq_iterate
- FunLike.semiring
- FunLike.monoidWithZero
- ContinuousLinearMap.one_apply
- ContinuousLinearMap.coe_pow'
- FunLike.coe_intCast
- FunLike.ring
- FunLike.coe_natCast
- FunLike.coe_one_eq_id_iff
Ancestors0
No ancestors.