transcendental — Mathlib

English

If x: ι → A is algebraically independent over R, then every x_i is transcendental over R.

Русский

Если x: ι → A является алгебраически независимым над R, то каждый x_i трансцендентен над R.

LaTeX

$$$\forall i:\ ι,\ Transcendental R (x i)\text{ whenever } AlgebraicIndependent R x$$

Lean4

/-- If a family `x` is algebraically independent, then any of its element is transcendental. -/
theorem transcendental (i : ι) : Transcendental R (x i) :=
  by
  have := hx.comp ![i] (Function.injective_of_subsingleton _)
  have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at this
  rwa [← algebraicIndependent_iff_transcendental]

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