X_ne_zero

Mathlib.RingTheory.PowerSeries.Basic

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

← MathLib Explorer

English

For a nontrivial R, the indeterminate X in R⟦X⟧ is nonzero: X ≠ 0 when R is nontrivial.

Русский

Для ненулевого R переменная X в R⟦X⟧ не равна нулю: X ≠ 0, если R ненуль.

LaTeX

$$$[\text{Nontrivial } R] \Rightarrow X \neq 0$$$

Lean4

@[simp]
theorem X_ne_zero [Nontrivial R] : (X : R⟦X⟧) ≠ 0 := fun H => by
  simpa only [coeff_one_X, one_ne_zero, map_zero] using congr_arg (coeff 1) H

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

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

Разделы

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

Аффилиация

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