coe_exp — Mathlib

English

For a finite index set, exp 𝕂 x i = exp 𝕂 (x i).

Русский

Для конечного множества индексов имеет место $\\exp 𝕂 x_i = \\exp 𝕂(x_i)$.

LaTeX

$$$\\exp 𝕂 x i = \\exp 𝕂 (x i)$$$

Lean4

@[simp]
theorem _root_.Pi.coe_exp {ι : Type*} {𝔸 : ι → Type*} [Finite ι] [∀ i, NormedRing (𝔸 i)] [∀ i, NormedAlgebra 𝕂 (𝔸 i)]
    [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) (i : ι) : exp 𝕂 x i = exp 𝕂 (x i) :=
  let ⟨_⟩ := nonempty_fintype ι
  map_exp _ (Pi.evalRingHom 𝔸 i) (continuous_apply _) x

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