gcd_map — Mathlib

English

For polynomials p and q, gcd after mapping via f equals the map of gcd: gcd(p.map f, q.map f) = (gcd p q).map f.

Русский

Для многочленов p и q примерно выполняется: gcd(p.map f, q.map f) = map f (gcd p q).

LaTeX

$$$ \gcd(p.map f, q.map f) = (\gcd p q).map f $$$

Lean4

theorem gcd_map [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) : gcd (p.map f) (q.map f) = (gcd p q).map f :=
  GCD.induction p q (fun x => by simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left]) fun x y _ ih => by
    rw [gcd_val, ← map_mod, ih, ← gcd_val]

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