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

mapDelta_diff_toZ

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)

 123lemma mapDelta_diff_toZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
 124  (p q : DeltaSub δ) :
 125  mapDelta δ hδ f p - mapDelta δ hδ f q
 126    = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by

proof body

Term-mode proof.

 127  classical
 128  simpa using (mapDelta_diff (δ:=δ) (hδ:=hδ) (f:=f) (p:=p) (q:=q))
 129
 130end UnitMapping
 131end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.