English
For any ring hom f:R → S and polynomial p ∈ R[X], degree (map f p) equals degree p if and only if f(leadingCoeff p) ≠ 0 or p = 0.
Русский
Для отображения f: R → S и полинома p ∈ R[X], deg(map f p) равно deg p тогда и только тогда, когда f(leadingCoeff p) ≠ 0 либо p = 0.
LaTeX
$$$\deg(\operatorname{map} f p) = \deg p \iff f(\operatorname{leadingCoeff} p) \neq 0 \lor p = 0$$$
Lean4
@[simp]
theorem degree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
degree (map f p) = degree p ↔ f (leadingCoeff p) ≠ 0 ∨ p = 0 :=
by
rcases eq_or_ne p 0 with h | h
· simp [h]
simp only [h, or_false]
refine ⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩
have h3 : natDegree (map f p) = natDegree p := by simp_rw [natDegree, h2]
have h4 : map f p ≠ 0 := by rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]
