leadingCoeff_opRingEquiv — Mathlib

English

The leading coefficient under the opposite-ring isomorphism is mapped to the opposite of the leading coefficient.

Русский

Префикс ведущего коэффициента в отображении противоположного кольца соответствует противоположному ведущему коэффициенту.

LaTeX

$$$(\operatorname{opRingEquiv} R p).\text{leadingCoeff} = \operatorname{op}(p.\text{leadingCoeff})$$$

Lean4

@[simp]
theorem leadingCoeff_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).leadingCoeff = op (unop p).leadingCoeff := by
  rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]

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