trdeg_of_isDomain

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

← MathLib Explorer

English

If R is a domain, then trdeg R (Polynomial R) equals 1.

Русский

Если R — домен, то трансцендентный размер трезования тривиального полинома равен 1.

LaTeX

$$$ [IsDomain R] \\Rightarrow trdeg R (Polynomial R) = 1 $$$

Lean4

@[simp]
theorem trdeg_of_isDomain [IsDomain R] : trdeg R (Polynomial R) = 1 := by
  simpa using (IsTranscendenceBasis.polynomial Unit R).lift_cardinalMk_eq_trdeg.symm

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

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

Разделы

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

Аффилиация

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