No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
77def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
proof body
Definition body.
78
79namespace LogicInt
80
81/-- Constructor: form an integer from a pair of naturals. -/
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
-
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
-
toInt_neg
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
… and 10 more
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
setoid
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
setoid
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
LogicInt
in IndisputableMonolith.NumberTheory.LogicLedgerInterop
decl_use