abbrev definition def or abbrev

`LogicInt`

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

formal statement (Lean)

  18abbrev LogicInt := Foundation.IntegersFromLogic.LogicInt

used by (40)

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

add in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_assoc' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_comm' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_left_neg' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_mul' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
add_zero' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
eq_iff_toInt_eq in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
equivInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
fromInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
fromInt_toInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
LogicInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mk in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_add' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_assoc' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_comm' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_eq_zero in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_one' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
mul_right_cancel in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
neg in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
ofLogicNat in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
ofLogicNat_zero in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
one_mul' in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
setoid in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
sound in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt_add in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toIntCore_respects in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
toInt_mul in IndisputableMonolith.Foundation.IntegersFromLogic decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

LogicInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use