isAdjoinRootMonic_map_eq_mk — Mathlib

English

For any natural n with n < natDegree f, the image of h.root^n under modByMonicHom equals X^n, i.e., h.modByMonicHom(h.root^n) = X^n.

Русский

Для любого n < natDegree f образ корня в modByMonicHom равен X^n: h.modByMonicHom(h.root^n) = X^n.

LaTeX

$$$ h.modByMonicHom (h.root^n) = X^n $$$

Lean4

@[deprecated "Use `simp` and `isAdjoinRoot_map_eq_mkₐ` instead" (since := "2025-08-07")]
theorem isAdjoinRootMonic_map_eq_mk (hf : f.Monic) : (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f := by
  simp [isAdjoinRoot_map_eq_mkₐ]

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