weierstrassMod_zero_left

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

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

← MathLib Explorer

English

Identity f = g·(f /ʷ g) + (f %ʷ g) holds.

Русский

Необходимо выполнить: f = g·(f /ʷ g) + (f %ʷ g).

LaTeX

$$f = g \cdot (f /ʷ g) + (f %ʷ g)$$

Lean4

@[simp]
theorem weierstrassMod_zero_left [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : 0 %ʷ g = 0 :=
  by
  simp_rw [weierstrassMod]
  split_ifs <;> simp

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

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

Разделы

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

Аффилиация

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