X_ne_C

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.X_ne_C

English

For any a ∈ R, X ≠ C(a) when R is nontrivial.

Русский

Для любого a ∈ R, X ≠ C(a) при ненулевом R.

LaTeX

$$$ X \neq C(a) \quad \text{for all } a \in R$$$

Lean4

theorem X_ne_C [Nontrivial R] (a : R) : X ≠ C a := by
  intro he
  simpa using monomial_eq_monomial_iff.1 he

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

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

Разделы

Аффилиация

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