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.

theorem Nat.cast_withTop (n : ) :
n = n
theorem Nat.cast_withBot (n : ) :
n = n