English
For any ring hom f:R → S and p ∈ R[X], natDegree (map f p) equals natDegree p if and only if f(leadingCoeff p) ≠ 0 or natDegree p = 0.
Русский
Для отображения f: R → S и полинома p ∈ R[X], natDegree(map f p) = natDegree p тогда и только тогда, когда f(leadingCoeff p) ≠ 0 или natDegree p = 0.
LaTeX
$$$\operatorname{natDegree}(\operatorname{map} f p) = \operatorname{natDegree}(p) \iff f(\operatorname{leadingCoeff} p) \neq 0 \lor \operatorname{natDegree}(p) = 0$$$
Lean4
@[simp]
theorem natDegree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
natDegree (map f p) = natDegree p ↔ f (p.leadingCoeff) ≠ 0 ∨ natDegree p = 0 :=
by
rcases eq_or_ne (natDegree p) 0 with h | h
· simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]
