toZ_one

formal source

 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
 146
 147/-- Map δ-subgroup to ℝ by composing an affine map with a provided projection to ℤ. -/
 148noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0)