of_ringHom_of_comp_eq — Mathlib

English

For an algebra homomorphism f: A →ₐ[R] B, IsAlgebraic(R, f(a)) is equivalent to IsAlgebraic(R, a) for any a ∈ A, provided f is injective.

Русский

Для гомоморфизма A →ₐ[R] B тождественно IsAlgebraic(R, f(a)) эквивалентно IsAlgebraic(R, a) при условии инъективности f.

LaTeX

$$$\forall f: A \to_R B,\; \text{Injective}(f)\Rightarrow \forall a:\, A,\ IsAlgebraic(R, f(a)) \iff IsAlgebraic(R, a).$$$

Lean4

theorem of_ringHom_of_comp_eq (H : Transcendental S (g a)) (hf : Function.Injective f)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Transcendental R a := fun halg ↦
  H (halg.ringHom_of_comp_eq f g hf h)

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