snd_exp

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#Prod.snd_exp

English

If x ∈ A × B, then (exp 𝕂 x).snd = exp 𝕂 x.snd.

Русский

Если x ∈ A × B, то (exp 𝕂 x).snd = exp 𝕂(x.snd).

LaTeX

$$$(\\exp 𝕂 x).snd = \\exp 𝕂 x.snd$$$

Lean4

@[simp]
theorem _root_.Prod.snd_exp [CompleteSpace 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).snd = exp 𝕂 x.snd :=
  map_exp _ (RingHom.snd 𝔸 𝔹) continuous_snd x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru