English
If x is transcendental over S and R injects into S, then x is transcendental over R.
Русский
Если x трансцендентен над S, и R инъективно вкладывается в S, то x трансцендентен над R.
LaTeX
$$$\text{Injective }(\mathrm{algebraMap}\ R\ S) \Rightarrow (\mathrm{Transcendental}\ S\ x \Rightarrow \mathrm{Transcendental}\ R\ x)$$$
Lean4
/-- If `x` is transcendental over `S`, then `x` is transcendental over `R` when `S` is an extension
of `R`, and the map from `R` to `S` is injective. -/
theorem restrictScalars (hinj : Function.Injective (algebraMap R S)) {x : A} (h : Transcendental S x) :
Transcendental R x := fun H ↦ h (H.extendScalars hinj)