reverse_natDegree_le — Mathlib

English

For every f ∈ R[X], (reverse f).natDegree ≤ f.natDegree.

Русский

Для каждого f ∈ R[X] natDegree(reverse f) ≤ natDegree(f).

LaTeX

$$$\operatorname{natDegree}(\operatorname{reverse}(f)) \le \operatorname{natDegree}(f).$$$

Lean4

theorem reverse_natDegree_le (f : R[X]) : f.reverse.natDegree ≤ f.natDegree :=
  by
  rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]
  intro n hn
  rw [Nat.cast_lt] at hn
  rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn), coeff_eq_zero_of_natDegree_lt hn]

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