English
If R → S is injective and A is algebraic over R, then A is algebraic over S.
Русский
Если сущетсвует инъекция R → S и A алгебраичен над R, то A алгебраичен над S.
LaTeX
$$$\forall {R,S,A}\ [\text{CommRing } R][\text{CommRing } S][\text{Ring } A]\ (\mathrm{Injective}(\mathrm{algebraMap}\ R\ S)) \rightarrow (\mathrm{Algebra.IsAlgebraic}\ R\ A \Rightarrow \mathrm{Algebra.IsAlgebraic}\ S\ A)$$$
Lean4
/-- If `x` is algebraic over `R`, then `x` is algebraic over `S` when `S` is an extension of `R`,
and the map from `R` to `S` is injective. -/
theorem extendScalars (hinj : Function.Injective (algebraMap R S)) {x : A} (A_alg : IsAlgebraic R x) :
IsAlgebraic S x :=
let ⟨p, hp₁, hp₂⟩ := A_alg
⟨p.map (algebraMap _ _), by rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩
