instNeg

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instNeg

English

The additive inverse in the quotient is induced by negation in the base ring: -[a] = [-a].

Русский

Приводимое к кольцу-остатку отрицание определяется через отрицание в исходном кольце: -[a] = [-a].

LaTeX

$$$-[a] = [-a]$$$

Lean4

instance {R : Type uR} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) :=
  ⟨neg r⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru