mirror_natTrailingDegree — Mathlib

English

The natTrailingDegree is preserved under mirroring: p.mirror.natTrailingDegree = p.natTrailingDegree.

Русский

natTrailingDegree сохраняется под зеркалированием: p.mirror.natTrailingDegree = p.natTrailingDegree.

LaTeX

$$$ p.mirror.natTrailingDegree = p.natTrailingDegree $$$

Lean4

theorem mirror_natTrailingDegree : p.mirror.natTrailingDegree = p.natTrailingDegree :=
  by
  by_cases hp : p = 0
  · rw [hp, mirror_zero]
  · rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp), natTrailingDegree_reverse, zero_add]

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