Theorems · Inductive type · logic and foundations
Unique
Sort u → Sort (max 1 u)
Unique α expresses that α is a type with a unique term default.
This is implemented as a type, rather than a Prop-valued predicate,
for good definitional properties of the default term.
- Defined in
- Mathlib.Logic.Unique
- Cited by
- 400 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by583
Results whose statement or proof uses this declaration.
- Finset.univ_uniquestatement and proof · cited by 94
- Fintype.card_uniquestatement and proof · cited by 59
- Unique.eq_defaultstatement and proof · cited by 38
- uniqueElimstatement and proof · cited by 29
- Equiv.funUniquestatement and proof · cited by 22
- MvPolynomial.uniqueAlgEquivstatement and proof · cited by 19
- ciSup_uniquestatement and proof · cited by 16
- Matrix.det_uniquestatement and proof · cited by 15
- Module.Basis.singletonstatement and proof · cited by 15
- Cardinal.mk_eq_oneproof · cited by 14
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalencestatement and proof · cited by 13
- Unique.forall_iffstatement and proof · cited by 13
Showing the 200 most cited of 583.