module module

`IndisputableMonolith.Foundation.ArithmeticFromLogic`

show as: view Lean formalization →

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

generate prose now

used by (8)

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

IndisputableMonolith.Foundation.ArithmeticOf module_import
IndisputableMonolith.Foundation.IntegersFromLogic module_import
IndisputableMonolith.Foundation.LogicRealization module_import
IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer module_import
IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit module_import
IndisputableMonolith.Foundation.TimeAsOrbit module_import
IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase module_import
IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import

declarations in this module (72)

inductive LogicNat L66
def zero L77
def succ L80
theorem zero_ne_succ L89
theorem succ_ne_zero L93
theorem succ_injective L99
theorem induction L106
def add L124
theorem add_def L132
theorem zero_def L133
theorem one_def L134
theorem add_zero L136
theorem add_succ L138
theorem zero_add L140
theorem succ_add L147
theorem add_assoc L154
theorem add_comm L161
def mul L171
theorem mul_def L177
theorem mul_zero L179
theorem mul_succ L181
theorem zero_mul L183
theorem mul_one L190
theorem one_mul L194
theorem mul_add L203
def toNat L221
def fromNat L226
theorem toNat_zero L230
theorem toNat_succ L231
theorem fromNat_zero L232
theorem fromNat_succ L233
theorem fromNat_toNat L235
theorem toNat_fromNat L243
def equivNat L253
theorem toNat_add L261
theorem toNat_mul L274
theorem add_left_cancel L286
theorem add_right_cancel L295
theorem eq_iff_toNat_eq L302
def le L325
def lt L328
theorem le_def L333
theorem lt_def L334
theorem le_refl L336
theorem zero_le L338
theorem le_trans L340
theorem le_succ L346
theorem succ_le_succ L350
theorem lt_iff_succ_le L356
theorem lt_irrefl L375
theorem lt_trans L383
theorem zero_lt_succ L387
theorem lt_iff_le_and_ne L390
theorem le_antisymm L409
theorem toNat_le L452
theorem toNat_lt L472
structure back L513
structure Generator L529
def generatorOfLawsOfLogic L541
def embed L556
theorem embed_zero L560
theorem embed_succ L562
theorem embed_pos L566
theorem embed_add L576
theorem embed_eq_pow L588
theorem log_generator_ne_zero L608
theorem embed_injective L620
theorem pow_le_pow_iff_of_one_lt L650
theorem pow_lt_pow_iff_of_one_lt L662
theorem embed_le_iff_of_one_lt L674
theorem embed_lt_iff_of_one_lt L679
theorem embed_strictMono_of_one_lt L684