Theorems · Theorem · field theory

Polynomial.map_mod_divByMonic

∀ {R : Type u} {S : Type v} [inst : Ring R] {p q : Polynomial R} [inst_1 : Ring S] (f : R →+* S),
  q.Monic →
    Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q ∧
      Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

2 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRing