ne_zero_of_coeff_ne_zero

Mathlib.RingTheory.HahnSeries.Basic

URI: https://scilib.ai/kg/mathlib#HahnSeries.ne_zero_of_coeff_ne_zero

← MathLib Explorer

English

If a coefficient x.coeff g is nonzero, then the Hahn series x is nonzero.

Русский

Если коэффициент ряда Хана при g не равен нулю, то сам ряд не равен нулю.

LaTeX

$$$\\text{if } x_{g} \\neq 0 \\text{ then } x \\neq 0$$$

Lean4

theorem ne_zero_of_coeff_ne_zero {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) : x ≠ 0 :=
  mt (fun x0 => (x0.symm ▸ coeff_zero : x.coeff g = 0)) h

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

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

Разделы

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

Аффилиация

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