lemma proved wrapper

`rungOf_fromZ`

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

formal statement (Lean)

  72@[simp] lemma rungOf_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  73  rungOf δ (fromZ δ n) = n := by

One-line wrapper that applies simpa.

  74  simpa [rungOf, toZ_fromZ δ hδ]
  75

Lean names referenced from this declaration's body.