snd_exp

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

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

English

The second component of the exponential equals exp 𝕜 x.fst times x.snd.

Русский

Вторая компонента экспоненты равна exp 𝕜 x.fst умножить на x.snd.

LaTeX

$$$\\mathrm{snd}(\\operatorname{exp}_{𝕜}(x)) = \\operatorname{exp}_{𝕜}(x.fst) \\cdot x.snd$$$

Lean4

@[simp]
theorem snd_exp (x : tsze R M) : snd (exp 𝕜 x) = exp 𝕜 x.fst • x.snd := by
  rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]

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

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

Разделы

Аффилиация

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