English
If R ⊆ S injectively and A is algebraic over R, then A is algebraic over S.
Русский
Если R → S инъективно и A алгебраичен над R, то A алгебраичен над S.
LaTeX
$$$\forall {R}\ {S}\ {A}\ [\mathrm{CommRing}\ R][\mathrm{CommRing}\ S][\mathrm{Ring}\ A]\ [\mathrm{Algebra}\ R\ S] [\mathrm{Algebra}\ S\ A] [\mathrm{Algebra}\ R\ A]\ (\mathrm{Injective}(\mathrm{algebraMap}\ R\ S) ) \Rightarrow (\mathrm{Algebra.IsAlgebraic}\ R\ A \Rightarrow \mathrm{Algebra.IsAlgebraic}\ S\ A)$$$
Lean4
/-- If A is an algebraic algebra over R, then A 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)) [Algebra.IsAlgebraic R A] :
Algebra.IsAlgebraic S A :=
⟨fun _ ↦ (Algebra.IsAlgebraic.isAlgebraic _).extendScalars hinj⟩
