mem_ker_modByMonic — Mathlib

English

If q is monic, then p lies in the kernel of the remainder map modulo q if and only if q divides p.

Русский

Пусть q монический; тогда p лежит в ядре отображения остатка по q тогда и только тогда, когда q делит p.

LaTeX

$$$$ p \\in \\ker\\big( \\text{modByMonicHom}(q) \\big) \\;\\iff\\; q \\mid p. $$$$

Lean4

theorem mem_ker_modByMonic (hq : q.Monic) {p : R[X]} : p ∈ LinearMap.ker (modByMonicHom q) ↔ q ∣ p :=
  LinearMap.mem_ker.trans (modByMonic_eq_zero_iff_dvd hq)

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