Theorems · Definition
DFunLike.coe
{F : Sort u_1} → {α : outParam (Sort u_2)} → {β : outParam (α → Sort u_3)} → [self : DFunLike F α β] → F → (a : α) → β aThe coercion from F to a function.
- Defined in
- Mathlib.Data.FunLike.Basic
- Cited by
- 62,936 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- DFunLike
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.
- DFunLikestatement and proof · cited by 576
Cited by69,794
Results whose statement or proof uses this declaration.
- MeasureTheory.aeproof · cited by 2,352
- Module.finrankproof · cited by 1,770
- MeasureTheory.Measure.restrictproof · cited by 1,646
- LinearMap.compproof · cited by 1,642
- Polynomial.Xproof · cited by 1,639
- map_zerostatement · cited by 1,614
- LinearEquiv.symmproof · cited by 1,461
- TensorProduct.tmulproof · cited by 1,182
- map_mulstatement · cited by 1,137
- Polynomial.coeffproof · cited by 1,045
- map_addstatement · cited by 964
- Real.logproof · cited by 939
Showing the 200 most cited of 69,794.