Commit 2024-09-15 23:33 2f80b44a

View on Github →

chore: split linear_combination (#16831) Split the lemmas in Mathlib.Tactic.LinearCombination into a new file, Mathlib.Tactic.LinearCombination.Lemmas.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/LinearCombination.lean

deleted theorem Mathlib.Tactic.LinearCombination.add_pf

deleted theorem Mathlib.Tactic.LinearCombination.c_mul_pf

deleted theorem Mathlib.Tactic.LinearCombination.eq_of_add

deleted theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow

deleted theorem Mathlib.Tactic.LinearCombination.eq_of_sub

deleted theorem Mathlib.Tactic.LinearCombination.pf_div_c

deleted theorem Mathlib.Tactic.LinearCombination.pf_mul_c

Created Mathlib/Tactic/LinearCombination/Lemmas.lean

added theorem Mathlib.Tactic.LinearCombination.add_pf

added theorem Mathlib.Tactic.LinearCombination.c_mul_pf

added theorem Mathlib.Tactic.LinearCombination.eq_of_add

added theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow

added theorem Mathlib.Tactic.LinearCombination.eq_of_sub

added theorem Mathlib.Tactic.LinearCombination.pf_div_c

added theorem Mathlib.Tactic.LinearCombination.pf_mul_c

Modified scripts/noshake.json