modByMonicHom — Mathlib

English

The remainder modulo a monic polynomial q induces an R-linear map from R[X] to R[X], given by p ↦ p modₘ q.

Русский

Остаток по модулю моного многочлена q задаёт линейное отображение над R: p ↦ p modₘ q.

LaTeX

$$$$ \\text{modByMonicHom}(q): \\; R[X] \\to_{R} R[X], \\; p \\mapsto p \\bmod_{\\! m} q. $$$$

Lean4

/-- `_ %ₘ q` as an `R`-linear map. -/
@[simps]
def modByMonicHom (q : R[X]) : R[X] →ₗ[R] R[X] where
  toFun p := p %ₘ q
  map_add' := add_modByMonic
  map_smul' := smul_modByMonic

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