instPow — Mathlib

English

Powers are preserved under toProd: (a^n).toProd = a.toProd^n.

Русский

Степени сохраняются под toProd: (a^n).toProd = a.toProd^n.

LaTeX

$$$ (a^n).toProd = a.toProd^n $$$

Lean4

instance instPow : Pow 𝓜(𝕜, A) ℕ where
  pow a
    n :=
    ⟨a.toProd ^ n, fun x y => by
      induction n generalizing x y with
      | zero => rfl
      | succ k hk =>
        rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
        rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]⟩

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