module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational`

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 (26)

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic module_import

declarations in this module (175)

def truncatedSub L36
def leq L42
def absDiff L48
theorem toNat_truncatedSub L52
theorem leq_eq_true_iff L68
theorem leq_eq_false_iff L86
theorem toNat_absDiff L92
structure SignedOrbit L130
def toInt L138
theorem toInt_mk L141
def zero L146
theorem zero_toInt L149
def one L154
theorem one_toInt L157
def ofOrbit L162
theorem ofOrbit_toInt L165
def add L171
theorem add_pos L175
theorem add_neg L178
theorem add_toInt L181
def negate L192
theorem negate_pos L196
theorem negate_neg L199
theorem negate_toInt L202
def mul L210
theorem mul_pos L214
theorem mul_neg L217
theorem mul_toInt L220
def sub L233
theorem sub_toInt L236
def scaleByNat L243
theorem scaleByNat_pos L247
theorem scaleByNat_neg L250
theorem scaleByNat_toInt L253
def balanced L266
instance instDecidableBalanced L269
theorem balanced_iff_toNat_eq L275
theorem balanced_iff_toInt_eq L291
theorem balanced_refl L301
theorem balanced_symm L305
theorem balanced_trans L310
theorem balanced_equivalence L315
def nonneg L324
def nonnegFlag L328
def negativeFlag L332
def le L336
def lt L340
def abs L344
theorem nonnegFlag_eq_true_iff L347
theorem nonnegFlag_eq_false_iff L355
theorem nonneg_iff_toInt_nonneg L363
theorem nonnegFlag_eq_true_iff_nonneg L378
theorem negativeFlag_eq_true_iff_toInt_neg L382
theorem abs_toNat L401
theorem abs_eq_zero_iff_toInt_eq_zero L406
theorem abs_ne_zero_of_toInt_ne_zero L418
theorem abs_ne_zero_of_not_balanced_zero L424
theorem le_iff_toInt_le L432
theorem lt_iff_toInt_lt L438
def signedOrbitEquiv L447
theorem signedOrbitEquiv_equivalence L450
theorem signedOrbitEquiv_iff_toInt_eq L454
def signedOrbitSetoid L459
def PRCInt L466
def mk L472
theorem mk_eq_mk_of_balanced L502
theorem add_respects_balanced L510
theorem add_mk L529
theorem toInt_add L533
theorem negate_respects_balanced L541
theorem negate_mk L556
theorem toInt_negate L560
theorem toInt_injective L568
theorem mul_respects_balanced L578
theorem mul_mk L598
theorem toInt_mul L602
theorem toInt_sub L613
theorem add_comm L621
theorem add_assoc L625
theorem zero_add L630

… and 95 more