equiv'_toAlgHom — Mathlib

English

The algebra hom component of the equivalence equiv' is exactly liftHom g pb.gen h2.

Русский

Однородная часть алгебраического гомома эквивалентности equiv' совпадает с liftHom g pb.gen h2.

LaTeX

$$(equiv' g pb h1 h2).toAlgHom = AdjoinRoot.liftHom g pb.gen h2$$

Lean4

theorem equiv'_toAlgHom (h₁ : aeval (root g) (minpoly R pb.gen) = 0) (h₂ : aeval pb.gen g = 0) :
    (equiv' g pb h₁ h₂).toAlgHom = AdjoinRoot.liftHom g pb.gen h₂ :=
  rfl

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