smul_weierstrassDiv

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

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

← MathLib Explorer

English

Weierstrass division is compatible with scalar multiplication: (a·f)/ʷ g = a·(f/ʷ g).

Русский

Деление по Вайершстрасу совместимо с редукцией на скаляры: (a·f)/ʷ g = a·(f/ʷ g).

LaTeX

$$$(a \cdot f)/ʷ g = a \cdot (f/ʷ g)$$$

Lean4

@[simp]
theorem smul_weierstrassDiv [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : (a • f) /ʷ g = a • (f /ʷ g) :=
  by
  simp_rw [weierstrassDiv]
  split_ifs <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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