lemma proved term proof

`mapDeltaTime_fromZ_one`

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

formal statement (Lean)

 182@[simp] lemma mapDeltaTime_fromZ_one
 183  (U : Constants.RSUnits) (n : ℤ) :
 184  mapDeltaOne LedgerUnits.toZ_one (timeMap U) (LedgerUnits.fromZ_one n)
 185    = U.tau0 * (n : ℝ) := by

proof body

Term-mode proof.

 186  simp [mapDeltaOne, timeMap, add_comm]
 187
 188-- (no actionMap in minimal RSUnits)
 189
 190end Scales
 191
 192end RecogSpec
 193end IndisputableMonolith

depends on (18)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
add_comm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromZ_one in IndisputableMonolith.LedgerUnits decl_use
toZ_one in IndisputableMonolith.LedgerUnits decl_use
U in IndisputableMonolith.Recognition decl_use
fromZ_one in IndisputableMonolith.RecogSpec.Scales decl_use
mapDeltaOne in IndisputableMonolith.RecogSpec.Scales decl_use
timeMap in IndisputableMonolith.RecogSpec.Scales decl_use
toZ_one in IndisputableMonolith.RecogSpec.Scales decl_use
add_comm in IndisputableMonolith.Relativity.Fields.Scalar decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use
actionMap in IndisputableMonolith.UnitMapping decl_use
timeMap in IndisputableMonolith.UnitMapping decl_use