ne_zero

Mathlib.RingTheory.AlgebraicIndependent.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicIndependent.ne_zero

English

If the ambient ring R is nontrivial, and x is algebraically independent, then each x_i is nonzero.

Русский

Если кольцо R ненулевое, и x алгебраически независимо, то каждый x_i не равен нулю.

LaTeX

$$$[Nontrivial\\,R] \\Rightarrow \\forall i, x_i \\neq 0$$$

Lean4

theorem ne_zero [Nontrivial R] (i : ι) : x i ≠ 0 :=
  hx.linearIndependent.ne_zero i

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

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

Разделы

Аффилиация

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