Lemmas for the linear_combination tactic

These should not be used directly in user code.

theorem Mathlib.Tactic.LinearCombination.add_pf {α : Type u_1} {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} [Add α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.pf_mul_c {α : Type u_1} {a : α} {b : α} [Mul α] (p : a = b) (c : α) : a * c = b * c

theorem Mathlib.Tactic.LinearCombination.c_mul_pf {α : Type u_1} {b : α} {c : α} [Mul α] (p : b = c) (a : α) : a * b = a * c

theorem Mathlib.Tactic.LinearCombination.pf_div_c {α : Type u_1} {a : α} {b : α} [Div α] (p : a = b) (c : α) : a / c = b / c

theorem Mathlib.Tactic.LinearCombination.eq_of_add {α : Type u_1} {a : α} {a' : α} {b : α} {b' : α} [Add α] [IsRightCancelAdd α] (p : a = b) (H : a' + b = b' + a) : a' = b'

theorem Mathlib.Tactic.LinearCombination.eq_rearrange {G : Type u_3} [AddGroup G] {a : G} {b : G} : a - b = 0 → a = b

Alias of the forward direction of sub_eq_zero.

theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow {α : Type u_1} {a : α} {a' : α} {b : α} {b' : α} [Ring α] [NoZeroDivisors α] (n : ℕ) (p : a = b) (H : (a' - b') ^ n - (a - b) = 0) : a' = b'