extendScalars — Mathlib

English

If a is transcendental over R and S is integral over R (Algebra.IsIntegral R S), then a is transcendental over S as well.

Русский

Если a над R трансцендентен, а S интегрально над R (Algebra.IsIntegral R S), то a трансцендентен над S.

LaTeX

$$$\\text{Transcendental}_R(a) \\Rightarrow [\\text{Algebra.IsIntegral } R S] \\Rightarrow \\text{Transcendental}_S(a)$$$

Lean4

theorem extendScalars [Algebra.IsAlgebraic R S] : Transcendental S a :=
  by
  contrapose ha
  rw [Transcendental, not_not] at ha ⊢
  exact ha.restrictScalars _

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