dyadicMap_apply — Mathlib

English

For all integers m and elements p ∈ Submonoid.powers(2), dyadicMap(IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = m · powHalf (log p).

Русский

Для любых целых m и p ∈ Submonoid.powers(2) применяем dyadicMap к классику m/p; результат равен m · powHalf(log p).

LaTeX

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

Lean4

@[simp]
theorem dyadicMap_apply (m : ℤ) (p : Submonoid.powers (2 : ℤ)) :
    dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = m * powHalf (Submonoid.log p) := by
  rw [← Localization.mk_eq_mk']; rfl

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