Theorems · Definition
FunLike
Sort u_1 → Sort u_2 → Sort u_3 → Sort (max (max (max 1 u_1) u_2) u_3)
The class FunLike F α β (Function-Like) expresses that terms of type F
have an injective coercion to functions from α to β.
FunLike is the non-dependent version of DFunLike.
This typeclass is used in the definition of the homomorphism typeclasses,
such as ZeroHomClass, MulHomClass, MonoidHomClass, ....
- Defined in
- Mathlib.Data.FunLike.Basic
- Cited by
- 2,560 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLikeproof · cited by 576
Cited by3,278
Results whose statement or proof uses this declaration.
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- MeasureTheory.aestatement and proof · cited by 2,352
- map_zerostatement and proof · cited by 1,614
- map_mulstatement and proof · cited by 1,137
- map_addstatement and proof · cited by 964
- map_onestatement and proof · cited by 861
- RingHomClass.toRingHomstatement and proof · cited by 746
- Ideal.mapstatement and proof · cited by 692
- map_smulstatement and proof · cited by 566
- map_substatement and proof · cited by 565
- map_powstatement and proof · cited by 503
- map_sumstatement and proof · cited by 455
Showing the 200 most cited of 3,278.