`quantization`

proved

show as: view math explainer →

module: IndisputableMonolith.LedgerUnits
domain: LedgerUnits
line: 107 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerUnits on GitHub at line 107.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 104  rfl
 105
 106/-- Quantization: every element of the δ-subgroup has a unique integer coefficient. -/
 107theorem quantization {δ : ℤ} (hδ : δ ≠ 0) (x : DeltaSub δ) :
 108  ∃! (n : ℤ), x.val = n * δ :=
 109by
 110  classical
 111  -- Existence from `toZ_spec`
 112  refine ⟨toZ δ x, ?eq, ?uniq⟩
 113  · simpa [toZ_spec δ x]
 114  · intro m hm
 115    -- Uniqueness from `rep_unique`
 116    have h1 : x.val = toZ δ x * δ := toZ_spec δ x
 117    have h2 : x.val = m * δ := hm
 118    have : m * δ = toZ δ x * δ := by rw [← h2, h1]
 119    exact rep_unique (δ:=δ) hδ this
 120
 121end LedgerUnits
 122end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.