modByMonicHom_root_pow — Mathlib

English

For any n, h.modByMonicHom (h.root^n) equals X^n provided n is less than natDegree f; i.e., h.modByMonicHom (h.root^n) = X^n.

Русский

Для любого n, если n < natDegree f, то h.modByMonicHom (h.root^n) = X^n.

LaTeX

$$$ h.modByMonicHom (h.root^n) = X^n \quad (n < \operatorname{natDegree}(f)) $$$

Lean4

@[simp]
theorem modByMonicHom_root_pow {n : ℕ} (hdeg : n < natDegree f) : h.modByMonicHom (h.root ^ n) = X ^ n :=
  by
  nontriviality R
  rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.monic, degree_X_pow]
  contrapose! hdeg
  simpa [natDegree_le_iff_degree_le] using hdeg

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