Commit 2024-08-27 00:43 948f204f

View on Github →

chore: fork linear_combination to linear_combination' (#16166) This PR makes a copy linear_combination' of the tactic linear_combination. The primed version will be left as-is for backward compatibility, while the unprimed version will soon undergo some opinionated refactors. This PR also makes some minor corrections to the module docstring (of both versions). Zulip

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/LinearCombination'.lean

added inductive Mathlib.Tactic.LinearCombination'.Expanded

added theorem Mathlib.Tactic.LinearCombination'.add_pf

added theorem Mathlib.Tactic.LinearCombination'.c_add_pf

added theorem Mathlib.Tactic.LinearCombination'.c_div_pf

added theorem Mathlib.Tactic.LinearCombination'.c_mul_pf

added theorem Mathlib.Tactic.LinearCombination'.c_sub_pf

added theorem Mathlib.Tactic.LinearCombination'.div_pf

added def Mathlib.Tactic.LinearCombination'.elabLinearCombination'

added theorem Mathlib.Tactic.LinearCombination'.eq_of_add

added theorem Mathlib.Tactic.LinearCombination'.eq_of_add_pow

added theorem Mathlib.Tactic.LinearCombination'.eq_trans₃

added theorem Mathlib.Tactic.LinearCombination'.inv_pf

added theorem Mathlib.Tactic.LinearCombination'.mul_pf

added theorem Mathlib.Tactic.LinearCombination'.neg_pf

added theorem Mathlib.Tactic.LinearCombination'.pf_add_c

added theorem Mathlib.Tactic.LinearCombination'.pf_div_c

added theorem Mathlib.Tactic.LinearCombination'.pf_mul_c

added theorem Mathlib.Tactic.LinearCombination'.pf_sub_c

added theorem Mathlib.Tactic.LinearCombination'.sub_pf

Modified Mathlib/Tactic/LinearCombination.lean

Modified Mathlib/Tactic/Linter/UnusedTactic.lean

Created test/linear_combination'.lean

added def g