isNilpotent_reflect_iff — Mathlib

English

P is nilpotent iff its reverse is nilpotent.

Русский

Полином P нильпотентен тогда и только тогда, когда его отражение reverse нильпотентно.

LaTeX

$$IsNilpotent(P.reverse) ↔ IsNilpotent(P)$$

Lean4

@[simp]
theorem isNilpotent_reflect_iff {P : R[X]} {N : ℕ} (hN : P.natDegree ≤ N) : IsNilpotent (reflect N P) ↔ IsNilpotent P :=
  by
  simp only [Polynomial.isNilpotent_iff]
  refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩ <;> rcases le_or_gt i N with hi | hi
  · simpa [tsub_tsub_cancel_of_le hi] using h (N - i)
  · simp [coeff_eq_zero_of_natDegree_lt <| lt_of_le_of_lt hN hi]
  · simpa [hi, revAt_le] using h (N - i)
  · simpa [revAt_eq_self_of_lt hi] using h i

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