theorem Hex.DensePoly.Interpret.map_pseudoDivMod {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Zero F] [DecidableEq F] [One F] [Add F] [Sub F] [Mul F] (f : E → F) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : DensePoly E) : (map f hz (p.pseudoDivMod q).fst, map f hz (p.pseudoDivMod q).snd) = (map f hz p).pseudoDivMod (map f hz q)

Interpretation commutes with every fold in fraction-free pseudo-division, including the fixed leading-coefficient scaling after a defective degree drop.

@[simp]

theorem Hex.DensePoly.Interpret.map_pseudoExponent {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (p q : DensePoly E) : (map f hz p).pseudoExponent (map f hz q) = p.pseudoExponent q

theorem Hex.DensePoly.Interpret.map_pseudoDiv {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Zero F] [DecidableEq F] [One F] [Add F] [Sub F] [Mul F] (f : E → F) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : DensePoly E) : { multiplier := f (p.pseudoDiv q).multiplier, quotient := map f hz (p.pseudoDiv q).quotient, remainder := map f hz (p.pseudoDiv q).remainder } = (map f hz p).pseudoDiv (map f hz q)

The interpretation preserves the recorded multiplier and both outputs.

theorem Hex.DensePoly.Interpret.map_positivePseudoDiv {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Zero F] [DecidableEq F] [One F] [Add F] [Sub F] [Mul F] (f : E → F) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [Neg E] [Neg F] (hn : ∀ (a : E), f (-a) = -f a) (signE : E → Int) (signF : F → Int) (hsign : ∀ (a : E), signF (f a) = signE a) (p q : DensePoly E) : { multiplier := f (positivePseudoDiv signE p q).multiplier, quotient := map f hz (positivePseudoDiv signE p q).quotient, remainder := map f hz (positivePseudoDiv signE p q).remainder } = positivePseudoDiv signF (map f hz p) (map f hz q)

Positive sign correction preserves the multiplier, quotient and remainder together.

theorem Hex.DensePoly.Interpret.map_pseudoGcd {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [One E] [Add E] [Sub E] [Mul E] [Zero F] [DecidableEq F] [One F] [Add F] [Sub F] [Mul F] (f : E → F) (hz : ∀ (a : E), f a = 0 ↔ a = 0) (h1 : f 1 = 1) (ha : ∀ (a b : E), f (a + b) = f a + f b) (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : DensePoly E) : map f hz (p.pseudoGcd q) = (map f hz p).pseudoGcd (map f hz q)

The fraction-free gcd follows the same strictly descending remainder sequence.