dyadic — Mathlib

English

For all m ∈ ℤ and n ∈ ℕ, dyadicMap(IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m · powHalf n.

Русский

Для всех m ∈ ℤ и n ∈ ℕ, dyadicMap(IsLocalization.mk' (Localization (Submonoid.powers 2)) m (2^n)) = m · powHalf n.

LaTeX

$$$$ \mathrm{dyadicMap}\big(\mathrm{IsLocalization.mk}'(\mathrm{Localization}(\mathrm{Submonoid.powers}(2)))\ m\ (\mathrm{Submonoid.pow} 2\ n)\big) = m \cdot powHalf n. $$$$

Lean4

/-- We define dyadic surreals as the range of the map `dyadicMap`. -/
def dyadic : Set Surreal :=
  Set.range dyadicMap

Похожие утверждения