transcendental_ringHom_iff_of_comp_eq

English

If the algebra map from S to A is injective, then Transcendental R (algebraMap S A a) iff Transcendental R a.

Русский

Если алгебраическое отображение from S to A инъективно, тогда Transcendental R (algebraMap S A a) эквивалентно Transcendental R a.

LaTeX

$$$\text{Transcendental}(R, \text{algebraMap } S A(a)) \iff \text{Transcendental}(R, a)$$$

Lean4

theorem transcendental_ringHom_iff_of_comp_eq (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental S B ↔ Algebra.Transcendental R A := by
  simp_rw [Algebra.transcendental_iff_not_isAlgebraic, Algebra.isAlgebraic_ringHom_iff_of_comp_eq f g h]

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