English
For a field k and a ring hom f : R →+* k, x.map f divides y.map f if and only if x divides y in R[X].
Русский
При поле k и кольцо-гомоморфизме f: R →+* k, x.map f делит y.map f тогда, когда x делит y в R[X].
LaTeX
$$x.map f ∣ y.map f ↔ x ∣ y$$
Lean4
theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y :=
by
by_cases H : x = 0
· rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
·
classical
rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply, coe_normUnit_of_ne_zero H,
coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H), leadingCoeff_map, ← map_inv₀ f, ← map_C, ←
Polynomial.map_mul, map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
