Commit 2026-04-21 08:27 60c81925

View on Github →

chore: forbid prime (') in filenames, rename LinearCombination' (#35518) This PR renames Mathlib/Tactic/LinearCombination'.lean to LinearCombinationPrime.lean (and the corresponding test file), and adds a lint check to modulesOSForbidden to prevent future files with prime/apostrophe characters in their names. The ' character in filenames causes shell escaping issues in scripts (any find ... -name '*.lean' or similar pattern needs careful quoting to handle these files correctly). 🤖 Prepared with Claude Code

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Renamed Mathlib/Tactic/LinearCombination'.lean to Mathlib/Tactic/LinearCombinationPrime.lean

deleted inductive Mathlib.Tactic.LinearCombination'.Expanded

deleted theorem Mathlib.Tactic.LinearCombination'.add_pf

deleted theorem Mathlib.Tactic.LinearCombination'.c_add_pf

deleted theorem Mathlib.Tactic.LinearCombination'.c_div_pf

deleted theorem Mathlib.Tactic.LinearCombination'.c_mul_pf

deleted theorem Mathlib.Tactic.LinearCombination'.c_sub_pf

deleted theorem Mathlib.Tactic.LinearCombination'.div_pf

deleted def Mathlib.Tactic.LinearCombination'.elabLinearCombination'

deleted theorem Mathlib.Tactic.LinearCombination'.eq_of_add

deleted theorem Mathlib.Tactic.LinearCombination'.eq_of_add_pow

deleted theorem Mathlib.Tactic.LinearCombination'.eq_trans₃

deleted theorem Mathlib.Tactic.LinearCombination'.inv_pf

deleted theorem Mathlib.Tactic.LinearCombination'.mul_pf

deleted theorem Mathlib.Tactic.LinearCombination'.neg_pf

deleted theorem Mathlib.Tactic.LinearCombination'.pf_add_c

deleted theorem Mathlib.Tactic.LinearCombination'.pf_div_c

deleted theorem Mathlib.Tactic.LinearCombination'.pf_mul_c

deleted theorem Mathlib.Tactic.LinearCombination'.pf_sub_c

deleted theorem Mathlib.Tactic.LinearCombination'.sub_pf

added inductive Mathlib.Tactic.LinearCombinationPrime.Expanded

added theorem Mathlib.Tactic.LinearCombinationPrime.add_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.c_add_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.c_div_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.c_mul_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.c_sub_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.div_pf

added def Mathlib.Tactic.LinearCombinationPrime.elabLinearCombination'

added theorem Mathlib.Tactic.LinearCombinationPrime.eq_of_add

added theorem Mathlib.Tactic.LinearCombinationPrime.eq_of_add_pow

added theorem Mathlib.Tactic.LinearCombinationPrime.eq_trans₃

added theorem Mathlib.Tactic.LinearCombinationPrime.inv_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.mul_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.neg_pf

added theorem Mathlib.Tactic.LinearCombinationPrime.pf_add_c

added theorem Mathlib.Tactic.LinearCombinationPrime.pf_div_c

added theorem Mathlib.Tactic.LinearCombinationPrime.pf_mul_c

added theorem Mathlib.Tactic.LinearCombinationPrime.pf_sub_c

added theorem Mathlib.Tactic.LinearCombinationPrime.sub_pf

Modified Mathlib/Tactic/Linter/TextBased.lean

Modified Mathlib/Tactic/Linter/UnusedTactic.lean

Renamed MathlibTest/linear_combination'.lean to MathlibTest/linear_combination_prime.lean