lemma proved wrapper

`mapDeltaOne_step`

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

formal statement (Lean)

 177lemma mapDeltaOne_step (f : AffineMapZ) (n : ℤ) :
 178  mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one (n+1))
 179    - mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n) = f.slope := by

proof body

One-line wrapper that applies simp.

 180  simp [mapDeltaOne, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add]
 181

depends on (11)

Lean names referenced from this declaration's body.

add_assoc in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
add_comm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
mul_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromZ_one in IndisputableMonolith.LedgerUnits decl_use
toZ_one in IndisputableMonolith.LedgerUnits decl_use
AffineMapZ in IndisputableMonolith.RecogSpec.Scales decl_use
fromZ_one in IndisputableMonolith.RecogSpec.Scales decl_use
mapDeltaOne in IndisputableMonolith.RecogSpec.Scales decl_use
toZ_one in IndisputableMonolith.RecogSpec.Scales decl_use
add_comm in IndisputableMonolith.Relativity.Fields.Scalar decl_use
AffineMapZ in IndisputableMonolith.UnitMapping decl_use