Mathlib Map

Theorems · Definition · logic and foundations

Trunc.mk

{α : Sort u_1} → α → Trunc α

Constructor for Trunc α

Defined in
Mathlib.Data.Quot
Cited by
21 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DFinsupp.single · cited by 113DFinsupp.singleDFinsupp.mk · cited by 28DFinsupp.mkFinsupp.toDFinsupp · cited by 21Finsupp.toDFinsuppMultiset.toDFinsupp · cited by 17Multiset.toDFinsuppDFinsupp.equivFunOnFintype · cited by 11DFinsupp.equivFunOnFintypesigmaFinsuppEquivDFinsupp · cited by 8sigmaFinsuppEquivDFinsuppDFinsupp.mem_support_toFun · cited by 6DFinsupp.mem_support_toFunLinearMap.coe_det · cited by 6LinearMap.coe_detTrunc.induction_on · cited by 5Trunc.induction_onLinearMap.det_def · cited by 5LinearMap.det_defLinearMap.det_conj · cited by 5LinearMap.det_conjEquiv.Perm.truncSwapFactors · cited by 5Perm.truncSwapFactorsDFinsupp.induction · cited by 5DFinsupp.inductionContinuousLinearMap.continuous_det · cited by 4ContinuousLinearMap.conti…Trunc.map · cited by 3Trunc.mapTrunc · cited by 39TruncTrunc.mkCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Truncstatement · cited by 39

Cited by42

Results whose statement or proof uses this declaration.