def
definition
fromZ_one
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.Scales on GitHub at line 115.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
112def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
113
114/-- Embed ℤ into the δ=1 subgroup. -/
115def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
116
117/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
118def toZ_one (p : DeltaSub 1) : ℤ := p.val
119
120@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
121
122@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
123 cases p with
124 | mk x hx =>
125 apply Subtype.ext
126 rfl
127
128/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
129def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
130{ toFun := toZ_one
131, invFun := fromZ_one
132, left_inv := fromZ_toZ_one
133, right_inv := toZ_fromZ_one }
134
135end LedgerUnits
136
137/-! Affine maps for unit-to-scale projections -/
138namespace Scales
139
140/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
141structure AffineMapZ where
142 slope : ℝ
143 offset : ℝ
144
145@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset