def
definition
def or abbrev
mapDelta
show as:
view Lean formalization →
formal statement (Lean)
148noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0)
149 (toZ : {x : ℤ // ∃ n : ℤ, x = n * δ} → ℤ) (f : AffineMapZ) :
150 {x : ℤ // ∃ n : ℤ, x = n * δ} → ℝ :=
proof body
Definition body.
151 fun p => f.slope * ((toZ p) : ℝ) + f.offset
152
153/-- Context constructors: charge (quantum `qe`), time (τ0), and action (ħ). -/