neg_left

Mathlib.Algebra.Ring.Associated

URI: https://scilib.ai/kg/mathlib#Associated.neg_left

English

If a is associated to b, then a is associated to -b (negation distributes to the right).

Русский

Если a ассоциировано с b, то a ассоциировано с -b (правое отрицание).

LaTeX

$$$\\text{Associated}(a,b) \\Rightarrow \\text{Associated}(a,-b)$$$

Lean4

theorem neg_left (h : Associated a b) : Associated (-a) b :=
  let ⟨u, hu⟩ := h;
  ⟨-u, by simp [hu]⟩

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

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

Разделы

Аффилиация

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