support_opRingEquiv — Mathlib

English

The opposite-ring polynomial isomorphism preserves natDegree: natDegree((opRingEquiv p)) = natDegree(unop p).

Русский

Противоположный кольцевой изоморфизм сохраняет натуральную степень полинома.

LaTeX

$$$\operatorname{natDegree}((\operatorname{opRingEquiv} R\, p)) = \operatorname{natDegree}(\operatorname{unop} p)$$$

Lean4

@[simp]
theorem support_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).support = (unop p).support :=
  Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective

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