map_mod — Mathlib

English

For any field k and ring hom f, (p % q).map f = p.map f % q.map f.

Русский

Для любого поля k и отображения f, отображение остатка сохраняется: (p % q).map f = p.map f % q.map f.

LaTeX

$$$ (p \bmod q)^{f} = p^{f} \bmod q^{f} $$$

Lean4

theorem map_mod [Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f :=
  by
  by_cases hq0 : q = 0
  · simp [hq0]
  ·
    rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

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