fromZ
plain-language theorem explainer
fromZ supplies the integer n directly as an element of DeltaSub δ when that type is identified with ℤ. Ledger unit mappings cite it to embed coefficients without constructing multiples. The definition is the identity assignment n.
Claim. $fromZ(δ, n) := n$ where $ΔSub(δ) := ℤ$ is the abstract placeholder for the subgroup generated by δ.
background
In UnitMapping, DeltaSub δ is defined as the type ℤ, serving as an abstract placeholder for the subgroup generated by δ using integers for mapping only. This differs from the concrete subtype in LedgerUnits, where DeltaSub δ := {x : ℤ // ∃ n : ℤ, x = n * δ} and the corresponding fromZ builds the subtype element ⟨n * δ, ⟨n, rfl⟩⟩.
proof idea
The definition is a direct assignment fromZ δ n := n. It is a one-line identity in the placeholder model.
why it matters
It is invoked by equiv_delta in LedgerUnits as the invFun in the equivalence DeltaSub δ ≃ ℤ for nonzero δ. This supports downstream definitions such as fromNat, rungOf_fromZ, and kOf_fromZ that extract indices from the mapped elements. The placeholder enables the abstract integer handling needed before specializing to the δ = 1 case in the ledger units layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.