C_ne_zero

Mathlib.RingTheory.HahnSeries.Multiplication

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

English

If r ≠ 0 then C(r) ≠ 0 in HahnSeries Γ R.

Русский

Если r ≠ 0, то C(r) ≠ 0 в HahnSeries Γ R.

LaTeX

$$$ r \ne 0 \Rightarrow C(r) \ne 0 $$$

Lean4

theorem C_ne_zero {r : R} (h : r ≠ 0) : (C r : HahnSeries Γ R) ≠ 0 :=
  C_injective.ne_iff' C_zero |>.mpr h

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

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

Разделы

Аффилиация

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