lemma proved term proof

`mapDeltaTime_fromZ`

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

formal statement (Lean)

  96@[simp] lemma mapDeltaTime_fromZ (δ : ℤ) (hδ : δ ≠ 0)
  97  (U : Constants.RSUnits) (n : ℤ) :
  98  mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 * (n : ℝ) := by

proof body

Term-mode proof.

  99  classical
 100  have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n)
 101  simpa [mapDeltaTime, timeMap, add_comm] using h
 102

depends on (16)

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 in IndisputableMonolith.LedgerUnits decl_use
U in IndisputableMonolith.Recognition decl_use
timeMap in IndisputableMonolith.RecogSpec.Scales decl_use
add_comm in IndisputableMonolith.Relativity.Fields.Scalar decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use
fromZ in IndisputableMonolith.UnitMapping decl_use
mapDelta_fromZ in IndisputableMonolith.UnitMapping decl_use
mapDeltaTime in IndisputableMonolith.UnitMapping decl_use
timeMap in IndisputableMonolith.UnitMapping decl_use