hasPow — Mathlib

English

The canonical representative respects exponentiation: mk(i^n) = (mk i)^n for i in NumDenSameDeg 𝒜 x and n ∈ ℕ.

Русский

Канонический представитель сохраняет возведение в степень: mk(i^n) = (mk i)^n для i ∈ NumDenSameDeg 𝒜 x и n ∈ ℕ.

LaTeX

$$$\mathrm{mk}(i^n) = \mathrm{mk}(i)^n$$$

Lean4

instance hasPow : Pow (HomogeneousLocalization 𝒜 x) ℕ where
  pow z
    n :=
    (Quotient.map' (· ^ n) fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) =>
          by
          change Localization.mk _ _ = Localization.mk _ _
          simp only [num_pow, den_pow]
          convert congr_arg (fun z : at x => z ^ n) h <;> rw [Localization.mk_pow] <;> rfl :
        HomogeneousLocalization 𝒜 x → HomogeneousLocalization 𝒜 x)
      z

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