isAlgebraic_ringHom_iff_of_comp_eq

English

Given an injective g and a composition equality, Transcendental S (g a) is equivalent to Transcendental R a.

Русский

При инъективности g и равенстве композиции Transcendental(S, g(a)) эквивалентно Transcendental(R, a).

LaTeX

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

Lean4

theorem isAlgebraic_ringHom_iff_of_comp_eq (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.IsAlgebraic S B ↔ Algebra.IsAlgebraic R A :=
  ⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.surjective f) (EquivLike.injective g) h, fun H ↦
    H.ringHom_of_comp_eq f g (EquivLike.injective f) (EquivLike.surjective g) h⟩

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