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

mapDelta_fromZ

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)

  75@[simp] lemma mapDelta_fromZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
  76  mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope * (n : ℝ) + f.offset := by

proof body

Term-mode proof.

  77  classical
  78  simp [mapDelta, LedgerUnits.toZ_fromZ δ hδ]
  79

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.