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]