pith. machine review for the scientific record. sign in
theorem proved term proof

toInt_fromInt

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)

 207theorem toInt_fromInt : ∀ n : Int, toInt (fromInt n) = n := by

proof body

Term-mode proof.

 208  intro n
 209  cases n with
 210  | ofNat n =>
 211    show toInt (mk (LogicNat.fromNat n) LogicNat.zero) = (Int.ofNat n)
 212    rw [toInt_mk, toNat_fromNat, toNat_zero]
 213    simp [Int.ofNat]
 214  | negSucc n =>
 215    show toInt (mk LogicNat.zero (LogicNat.fromNat (Nat.succ n))) = Int.negSucc n
 216    rw [toInt_mk, toNat_zero, toNat_fromNat]
 217    simp [Int.negSucc_eq]
 218

used by (4)

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

depends on (12)

Lean names referenced from this declaration's body.