neg_add

Mathlib.Tactic.Ring.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Ring.neg_add

Lean4

theorem neg_add {R} [Ring R] {a₁ a₂ b₁ b₂ : R} (_ : -a₁ = b₁) (_ : -a₂ = b₂) : -(a₁ + a₂) = b₁ + b₂ := by subst_vars;
  simp [add_comm]

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

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

Разделы

Аффилиация

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