def definition def or abbrev

`toIntCore`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 180def toIntCore : LogicNat × LogicNat → Int :=

Definition body.

 181  fun p => (toNat p.1 : Int) - (toNat p.2 : Int)
 182

From the project-wide theorem graph. These declarations reference this one in their body.

toInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toIntCore_respects in IndisputableMonolith.Foundation.IntegersFromLogic decl_use

Lean names referenced from this declaration's body.