Commit 2025-08-29 13:16 5ebb0a7e

fix(to_additive): propagate reorder and relevant_arg in simps and structures (#29059) This PR fixes an issue in to_additive where the lemmas generated by (attr := simps) don't inherit the relevant_arg. Similarly, the projections/constuctors of structures don't inherit relevant_arg. To do this, we deprecate the syntax to_additive_relevant_arg ... in favour of the new syntax to_additive (relevant_arg := ...). The same information was being lost for (reorder := ...), so that is also addressed by this PR.