transcendental_iff_not_isAlgebraic

Mathlib.RingTheory.Algebraic.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.transcendental_iff_not_isAlgebraic

← MathLib Explorer

English

Algebra.Transcendental R A is equivalent to not Algebra.IsAlgebraic R A.

Русский

Algebra.Transcendental R A эквивалентно не Algebra.IsAlgebraic R A.

LaTeX

$$$\\text{Algebra.Transcendental}(R,A) \\iff \\lnot \\text{Algebra.IsAlgebraic}(R,A)$$$

Lean4

theorem transcendental_iff_not_isAlgebraic : Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A := by
  simp [isAlgebraic_def, transcendental_def, Transcendental]

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

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

Разделы

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

Аффилиация

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