algebraMap — Mathlib

English

If a is algebraic over R, then its image under algebraMap S A is algebraic over R.

Русский

Если a алгебраичен над R, то его образ под algebraMap S A алгебраичен над R.

LaTeX

$$$ IsAlgebraic R a \to IsAlgebraic R (algebraMap S A a) $$$

Lean4

protected theorem algebraMap {a : S} : IsAlgebraic R a → IsAlgebraic R (algebraMap S A a) := fun ⟨f, hf₁, hf₂⟩ =>
  ⟨f, hf₁, by rw [aeval_algebraMap_apply, hf₂, map_zero]⟩

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