coe_neg — Mathlib

English

If the ambient structure is a ring, the inclusion preserves negation: the image of -x equals the negation of the image of x.

Русский

Если окружение является кольцом, включение сохраняет отрицание: образ -x равен отрицанию образа x.

LaTeX

$$$ -(x)^{\\uparrow} = (-x)^{\\uparrow} \\quad (x \\in S). $$$

Lean4

protected theorem coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A}
    (x : S) : (↑(-x) : A) = -↑x :=
  rfl

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