transcendental_ringHom_iff_of_comp_eq

English

Transcendental S B is equivalent to Transcendental R A under a composition equivalence of ring maps.

Русский

Transcendental(S,B) эквивалентно Transcendental(R,A) при равенстве композиции кольцевых отображений.

LaTeX

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

Lean4

theorem transcendental_ringHom_iff_of_comp_eq (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) {a : A} :
    Transcendental S (g a) ↔ Transcendental R a :=
  not_congr (isAlgebraic_ringHom_iff_of_comp_eq f g hg h)

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