English
In a polynomial ring R[X] over a commutative ring, if the leadingCoeff of f is a unit and its image under a ring hom φ is a unit, then f is a unit.
Русский
В полиномиальной кольцевой области R[X], если ведущий коэффициент f является единицей, а образ под отображением φ тоже единица, то f является единицей.
LaTeX
$$$\\text{IsUnit}(f) \\,\\Leftarrow\\, \\text{IsUnit}(f.leadingCoeff) \\wedge \\text{IsUnit}(\\mathrm{map}\\, φ\\, f)$$$
Lean4
theorem isUnit_of_isUnit_leadingCoeff_of_isUnit_map (hf : IsUnit f.leadingCoeff) (H : IsUnit (map φ f)) : IsUnit f :=
by
have dz := degree_eq_zero_of_isUnit H
rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
· rw [eq_C_of_degree_eq_zero dz]
refine IsUnit.map C ?_
convert hf
change coeff f 0 = coeff f (natDegree f)
rw [(degree_eq_iff_natDegree_eq _).1 dz]
· rfl
rintro rfl
simp at H
· intro h
have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
rw [h] at u
simp at u
