Commit 2023-03-06 21:55 497ddaf7

View on Github →

fix: issues in linear_combination + polyrith (#2678) As reported on Zulip.

Estimated changes

Modified Mathlib/Tactic/LinearCombination.lean

modified theorem Mathlib.Tactic.LinearCombination.c_add_pf

modified theorem Mathlib.Tactic.LinearCombination.c_div_pf

modified theorem Mathlib.Tactic.LinearCombination.c_mul_pf

modified theorem Mathlib.Tactic.LinearCombination.c_sub_pf

Modified Mathlib/Tactic/Polyrith.lean

modified def Mathlib.Tactic.Polyrith.Poly.toSyntax

Modified test/linear_combination.lean