dyadicMap_apply_pow — 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

theorem dyadicMap_apply_pow (m : ℤ) (n : ℕ) :
    dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • powHalf n :=
  by
  rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]
  simp only [zsmul_eq_mul]

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