natDegree_map_lt' — Mathlib

English

A variant of natDegree_map_lt': if f(p.leadingCoeff) = 0 and 0 < natDegree p, then natDegree(p.map f) < natDegree p.

Русский

Вариант natDegree_map_lt': если f(p.leadingCoeff) = 0 и 0 < natDegree p, тогда natDegree(p.map f) < natDegree p.

LaTeX

$$$\\operatorname{natDegree}(p.map\\ f) < \\operatorname{natDegree}(p) \\quad\\text{(when } f(p.leadingCoeff)=0\\text{ and }0 < \\operatorname{natDegree}(p)\\)$$$

Lean4

/-- Variant of `natDegree_map_lt` that assumes `0 < natDegree p` instead of `map f p ≠ 0`. -/
theorem natDegree_map_lt' (hp : f p.leadingCoeff = 0) (hp₀ : 0 < natDegree p) : (p.map f).natDegree < p.natDegree :=
  by
  by_cases H : map f p = 0
  · rwa [H, natDegree_zero]
  · exact natDegree_map_lt hp H

Похожие утверждения