neg_def

Mathlib.RingTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.neg_def

English

Negation distributes over oreDiv: -(r /ₒ s) = (-r) /ₒ s.

Русский

Отрицание распределено по oreDiv: -(r /ₒ s) = (-r) /ₒ s.

LaTeX

$$ -(r /ₒ s) = (-r) /ₒ s$$

Lean4

@[simp]
protected theorem neg_def (r : X) (s : S) : -(r /ₒ s) = -r /ₒ s := by with_unfolding_all rfl

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

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

Разделы

Аффилиация

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