restrictScalars — Mathlib

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)

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