transcendental_X

Mathlib.RingTheory.Algebraic.MvPolynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.transcendental_X

← MathLib Explorer

English

For any i, X_i is transcendental over the base field R.

Русский

Для любого i элемент X_i трансцендентален над полем R.

LaTeX

$$$$ \forall i, \text{ Transcendental } R (X_i : MvPolynomial \sigma R). $$$$

Lean4

theorem transcendental_X (i : σ) : Transcendental R (X i : MvPolynomial σ R) := by
  simpa using transcendental_polynomial_aeval_X R i (Polynomial.transcendental_X R)

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

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

Разделы

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

Аффилиация

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