map_sin

Mathlib.RingTheory.PowerSeries.WellKnown

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

English

A ring homomorphism f respects the sine power series: map f (sin A) = sin A'.

Русский

Гомоморфизм сохраняет синусовую серию: map f (sin A) = sin A'.

LaTeX

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

Lean4

@[simp]
theorem map_sin : map f (sin A) = sin A' := by
  ext
  simp [sin, apply_ite f]

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

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

Разделы

Аффилиация

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