trdeg_pos — Mathlib

English

If there exists a transcendental element over R in A, then 0 < trdeg_R A.

Русский

Если существует трансцендентальный элемент над R в A, то 0 < trdeg_R A.

LaTeX

$$$[Algebra.Transcendental R A] \Rightarrow 0 < trdeg R A$$

Lean4

theorem trdeg_pos [Algebra.Transcendental R A] : 0 < trdeg R A :=
  have ⟨x, hx⟩ := Algebra.Transcendental.transcendental (R := R) (A := A)
  zero_lt_one.trans_le <|
    le_ciSup_of_le (Cardinal.bddAbove_range _) ⟨{ x }, algebraicIndependent_unique_type_iff.mpr hx⟩ (by simp)

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