Documentation

Mathlib.Data.Nat.Cast.WithTop

Lemma about the coercion ℕ → WithBot ℕ. #

An orphaned lemma about casting from ℕ to WithBot ℕ, exiled here during the port to minimize imports of Algebra.Order.Ring.Rat.

source
instance instWellFoundedRelationWithTopNat :
WellFoundedRelation (WithTop ℕ)
Equations
    source
    theorem Nat.cast_withTop (n : ℕ) :
    ↑n = ↑n
    source
    theorem Nat.cast_withBot (n : ℕ) :
    ↑n = ↑n