of_injective — Mathlib

English

If f: A →ₐ[R] B is injective and B is algebraic over R, then A is algebraic over R.

Русский

Если f инъективен и B алгебраичен над R, то и A алгебраичен над R.

LaTeX

$$$\text{IsAlgebraic}(R, B) \Rightarrow \text{IsAlgebraic}(R, A)$ via injective AlgHom f.$$

Lean4

theorem of_injective (f : A →ₐ[R] B) (hf : Function.Injective f) [Algebra.IsAlgebraic R B] : Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (isAlgebraic_algHom_iff f hf).mp (Algebra.IsAlgebraic.isAlgebraic _)⟩

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