power_sum — Mathlib

English

For any a and f, a^(sum f) = product over i of a^(f(i)).

Русский

Для любого a и f выполняется a^{sum f} = ∏_i a^{f(i)}.

LaTeX

$$$ a^{\sum f} = \prod_{i} a^{f(i)} $$$

Lean4

theorem power_sum {ι} (a : Cardinal) (f : ι → Cardinal) : a ^ sum f = prod fun i ↦ a ^ f i := by
  induction a using Cardinal.inductionOn with
  | _ α =>
    induction f using induction_on_pi with
    | _ f =>
      simp_rw [prod, sum, power_def]
      apply mk_congr
      refine (Equiv.piCurry fun _ _ => α).trans ?_
      refine Equiv.piCongrRight fun b => ?_
      refine (Equiv.arrowCongr outMkEquiv (Equiv.refl α)).trans ?_
      exact outMkEquiv.symm

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