algHom — Mathlib

English

Let f be an algebra homomorphism from A to B over R. If a ∈ A is algebraic over R, then f(a) is algebraic over R.

Русский

Пусть f — алгебраHom(A, B) над R. Если a ∈ A алгебраичен над R, то и f(a) алгебраичен над R.

LaTeX

$$$\forall f: A \to_R B, \; \forall a \in A, \; \IsAlgebraic(R, a) \Rightarrow \IsAlgebraic(R, f(a)).$$$

Lean4

/-- This is slightly more general than `IsAlgebraic.algebraMap` in that it
  allows noncommutative intermediate rings `A`. -/
protected theorem algHom (f : A →ₐ[R] B) {a : A} (h : IsAlgebraic R a) : IsAlgebraic R (f a) :=
  let ⟨p, hp, ha⟩ := h
  ⟨p, hp, by rw [aeval_algHom, f.comp_apply, ha, map_zero]⟩

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