Mathlib Map

Structures · Lean core

NatCast

The canonical homomorphism Nat → R. In most use cases, the target type will have a (semi)ring structure, and this homomorphism should be a (semi)ring homomorphism. NatCast and IntCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a NatCast R instance) whenever R is an additive monoid with a 1. The prototypical example is Int.ofNat.

Defined in
Init.Data.Cast
Shape
One type argument · adds natCast
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Concrete types that are instances50

  • Int
  • Nat
  • Real
  • Rat
  • Quiver.Hom
  • Complex
  • SeparationQuotient
  • BitVec
  • ContinuousLinearMap
  • Polynomial
  • Filter.Germ
  • BoundedContinuousFunction
  • Matrix
  • WithVal
  • HahnSeries
  • NonemptyInterval
  • LocallyConstant
  • ENat
  • MeasureTheory.SimpleFunc
  • RestrictedProduct
  • DirectSum
  • DoubleCentralizer
  • CauSeq.Completion.Cauchy
  • WittVector
  • CauSeq
  • TruncatedWittVector
  • LucasLehmer.X
  • FractionalIdeal
  • AdicCompletion
  • Cardinal
  • Representation.IntertwiningMap
  • AdicCompletion.AdicCauchySequence
  • RingCon.Quotient
  • HomogeneousLocalization
  • RingQuot
  • CentroidHom
  • ModularForm
  • SlashInvariantForm
  • Dyadic
  • Lean.Grind.Ring.OfSemiring.Q
  • FirstOrder.Language.Term
  • Subtype
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • ContinuousMap
  • WithTop
  • WithBot

How is a type an instance?

Loading the hierarchy index…

Assumed by139

Ancestors0

No ancestors.