trdeg_ne_zero_iff

Mathlib.RingTheory.AlgebraicIndependent.Transcendental

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

English

trdeg R A ≠ 0 if and only if A is transcendental over R.

Русский

trdeg R A не равно нулю тогда и только тогда, когда A трансцендентна над R.

LaTeX

$$$trdeg\ R\ A \neq 0 \iff Algebra.Transcendental R A$$

Lean4

theorem trdeg_ne_zero_iff : trdeg R A ≠ 0 ↔ Algebra.Transcendental R A := by
  rw [Algebra.transcendental_iff_not_isAlgebraic, Ne, trdeg_eq_zero_iff]

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

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

Разделы

Аффилиация

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