instNegSubtypeMemSubmonoid — Mathlib

English

In a ring with star, the unitary subtype is closed under additive negation; i.e., if U is unitary, then −U is unitary.

Русский

В кольце с звездой подтипу унитарных элементов свойственна замкнутость относительно сложения: если U унитарен, то −U тоже унитарен.

LaTeX

$$$U \in \mathrm{Unitary}(R) \Rightarrow -U \in \mathrm{Unitary}(R)$$$

Lean4

instance : Neg (unitary R) where neg U := ⟨-U, by simp [mem_iff, star_neg]⟩

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