trdeg_eq_zero

Mathlib.RingTheory.AlgebraicIndependent.Transcendental

URI: https://scilib.ai/kg/mathlib#trdeg_eq_zero

← MathLib Explorer

English

If A is algebraic over R, then trdeg_R A = 0.

Русский

Если A алгебраично над R, то trdeg_R A = 0.

LaTeX

$$$[Algebra.IsAlgebraic R A] : trdeg R A = 0$$

Lean4

theorem trdeg_eq_zero [Algebra.IsAlgebraic R A] : trdeg R A = 0 :=
  bot_unique <|
    ciSup_le' fun s ↦
      have := s.2.isEmpty_of_isAlgebraic;
      (Cardinal.mk_eq_zero _).le

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

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

Разделы

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

Аффилиация

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