infinite

Mathlib.RingTheory.Algebraic.Basic

URI: https://scilib.ai/kg/mathlib#Transcendental.infinite

English

If x is transcendental over R in A, then A is infinite.

Русский

Если x трансцендентен над R в A, то A бесконечно.

LaTeX

$$$\\text{Transcendental}(R,x) \\Rightarrow \\lvert A \\rvert = \\infty$$$

Lean4

theorem infinite {x : A} (hx : Transcendental R x) : Infinite A :=
  .of_injective _ (transcendental_iff_injective.mp hx)

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

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

Разделы

Аффилиация

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