natDegree_opRingEquiv — Mathlib

English

For p ∈ (R[X])ᵐᵒᵖ, the natDegree of opRingEquiv p equals the natDegree of unop p.

Русский

Для p ∈ (R[X])ᵐᵒᵖ, natDegree(опRingEquiv p) равно natDegree(unop p).

LaTeX

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

Lean4

@[simp]
theorem natDegree_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).natDegree = (unop p).natDegree :=
  by
  by_cases p0 : p = 0
  · simp only [p0, map_zero, natDegree_zero, unop_zero]
  ·
    simp only [p0, natDegree_eq_support_max', Ne, EmbeddingLike.map_eq_zero_iff, not_false_iff, support_opRingEquiv,
      unop_eq_zero_iff]

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