pith. machine review for the scientific record. sign in
def definition def or abbrev

reciprocalIntegerLedger_of_logicInt

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

formal statement (Lean)

  37def reciprocalIntegerLedger_of_logicInt
  38    {z : LogicInt}
  39    (h : LogicIntNonIdentityReciprocal z) :
  40    ReciprocalIntegerLedger where
  41  carrier := Int.natAbs (logicIntToInt z)

proof body

Definition body.

  42  carrier_pos := natAbs_pos_of_logicInt_pos h.pos
  43  nonidentity := by
  44    intro hcarrier
  45    have h_toInt_abs : Int.natAbs (logicIntToInt z) = 1 := hcarrier
  46    have h_toInt : logicIntToInt z = 1 := by
  47      have habs_cast : (Int.natAbs (logicIntToInt z) : Int) = 1 := by
  48        exact_mod_cast h_toInt_abs
  49      rw [Int.natAbs_of_nonneg (le_of_lt h.pos)] at habs_cast
  50      exact habs_cast
  51    exact h.nonidentity h_toInt
  52  has_reciprocal_budget := by
  53    rcases h.reciprocal_budget with ⟨N, _hNpos, hdiv⟩
  54    exact ⟨N, hdiv⟩
  55
  56/-- Recovered non-identity integer ledgers have a finite phase separating
  57them from identity. -/

used by (1)

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

depends on (16)

Lean names referenced from this declaration's body.