eq_of_add

Mathlib.Tactic.LinearCombination'

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LinearCombination'.eq_of_add

Lean4

theorem eq_of_add [AddGroup α] (p : (a : α) = b) (H : (a' - b') - (a - b) = 0) : a' = b' := by
  rw [← sub_eq_zero] at p ⊢; rwa [sub_eq_zero, p] at H

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

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

Разделы

Аффилиация

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