Mathlib Map

Structures · Logic and sets

Unique

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
Shape
One type argument · adds uniq
Open in Mathlib docs

Extends1

Extended by1

Forgetful instances

Every Unique is also a

Provided automatically by

Concrete types that are instances100

  • Quiver.Hom
  • TopCat.carrier
  • CategoryTheory.Functor.obj
  • ContinuousLinearMap
  • ZMod
  • Polynomial
  • CStarMatrix
  • TensorProduct
  • FractionRing
  • WithConv
  • Matrix
  • Units
  • WithLp
  • FreeAbelianGroup
  • MonoidAlgebra
  • ModuleCat.carrier
  • AddMonoidAlgebra
  • Finsupp
  • DirectSum
  • CategoryTheory.Discrete
  • SymAlg
  • Localization
  • SkewMonoidAlgebra
  • Interval
  • AddUnits
  • ContinuousAlternatingMap
  • DFinsupp
  • TopologicalSpace.NonemptyCompacts
  • PreLp
  • WithCStarModule
  • CategoryTheory.PreZeroHypercover.I₀
  • AlgEquiv
  • LieSubmodule
  • Associates
  • PrimeSpectrum
  • SimpleGraph
  • FreeGroup
  • Ordinal.ToType
  • CategoryTheory.ShrinkHoms
  • TopologicalSpace.Opens
  • FreeAddGroup
  • TopologicalSpace.Compacts
  • LinearEquiv
  • Digraph
  • AlternatingMap
  • Equiv.Perm
  • CategoryTheory.Quotient
  • PolynomialModule
  • AddSubgroup
  • CategoryTheory.Paths
  • DMatrix
  • AddCommGroup.DirectLimit
  • Abelianization
  • Module.DirectLimit
  • Polynomial.Gal
  • Sym2
  • AddSubmonoid
  • SSet.Truncated.HomotopyCategory
  • CategoryTheory.Cat.FreeRefl
  • AlgHom
  • Sublattice
  • BooleanSubalgebra
  • Sym
  • FreeMonoid
  • UniformSpace
  • GradedAlgHom
  • TopologicalSpace
  • WithTopology
  • SimpleGraph.ConnectedComponent
  • Function.Embedding
  • FreeAddMonoid
  • FirstOrder.Language.Symbols
  • SimpleGraph.Hom
  • TopologicalSpace.OpenNhdsOf
  • Partition
  • MaximalSpectrum
  • Finpartition
  • Flag
  • RingEquiv
  • OrderIso
  • AddEquiv
  • MulEquiv
  • NumberField.InfinitePlace
  • OrderAddMonoidIso
  • OrderMonoidIso
  • ContinuousAddEquiv
  • ContinuousMulEquiv
  • True
  • CategoryTheory.Iso
  • Field.Emb
  • CategoryTheory.ShortComplex.HomologyMapData
  • CategoryTheory.Functor.WellOrderInductionData.Extension
  • CategoryTheory.ShortComplex.RightHomologyMapData
  • CategoryTheory.ShortComplex.LeftHomologyMapData
  • Module.Basis
  • OrderedFinpartition
  • PresheafOfModules.Sheafify.SMulCandidate
  • Quiver.Path
  • Nat.Partition
  • FirstOrder.Language.LHom

How is a type an instance?

Loading the hierarchy index…

Assumed by501

Ancestors34