map_exp

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.map_exp

English

For ring homomorphism f: A →+* A', map f sends exp A to exp A'.

Русский

Пусть f: A →+* A' — кольцевой гомоморфизм; отображение экспоненты сохраняется: map f (exp A) = exp A'.

LaTeX

$$$$ map\, f\ (\exp A) = \exp A' $$$$

Lean4

@[simp]
theorem map_exp : map (f : A →+* A') (exp A) = exp A' := by
  ext
  simp

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

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

Разделы

Аффилиация

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