liftHom_mk — Mathlib

English

If f and g are Associated, there exists a canonical algebra isomorphism algEquivOfAssociated f g hfg : AdjoinRoot f ≃ₐ[R] AdjoinRoot g.

Русский

Если f и g ассоциированы, существует канонический алгебра-изоморфизм AdjoinRoot f ≃ₐ[R] AdjoinRoot g.

LaTeX

$$$\\text{AdjoinRoot } f \\simeq_{R} \\text{AdjoinRoot } g$$$

Lean4

@[simp]
theorem liftHom_mk {g : R[X]} : liftHom f a hfx (mk f g) = aeval a g :=
  lift_mk hfx g

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