neg_quot

Mathlib.Algebra.RingQuot

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

← MathLib Explorer

English

Negation in the quotient corresponds to negation in the base ring: -[a] = [-a].

Русский

Отрицание в кольце-остатке соответствует отрицанию в исходном кольце: -[a] = [-a].

LaTeX

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

Lean4

theorem neg_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a} : (-⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (-a)⟩ :=
  by
  change neg r _ = _
  rw [neg_def]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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