Moving/deprecating #align-ed theorems

Stream: mathlib4

[Emilie (Shad Amethyst)]

I'm implementing MulAction.period g a, which is a wrapper around Function.minimalPeriod (fun x => g • x) a, that allows for cleaner proofs (while remaining definitionally equal to the latter).
However, I only just noticed that MulAction.pow_smul_eq_iff_minimalPeriod_dvd is defined directly in Mathlib.Dynamics.PeriodicPts, and is already #align-ed.

I would like to know if it's possible to:

• move those theorems to the new module I created for that topic, Mathlib.GroupTheory.GroupAction.Period (breaking change, although the fix for it is easy)
• deprecate it (minor change, but an inconvenient one when relying on semver)
• move the #align over to the new versions of those theorems that use MulAction.period instead

Beyond that, is it acceptable to switch over more theorems using Function.minimalPeriod (fun x => g • x) a to MulAction.period g a? I'll be making these changes in a separate PR anyway.

[Eric Rodriguez]

The policy around breaking changes in mathlib is usually "fix any breakages within mathlib itself and you're good!" There's some discussion about being a bit more harsh than this around very core parts, but I don't think it's an issue here.

Increasing the import requirements of things is seen a bit more harshly, so that depends. Mathlib doesn't really use semver, as far as I'm aware.

I think you can toy with replacing it fully and see what happens.

[Eric Wieser]

Eric Rodriguez said:

The policy around breaking changes in mathlib is usually "fix any breakages within mathlib itself and you're good!"
<snip>
I think you can toy with replacing it fully and see what happens.

To be clear, this means "make the PR with a breaking change, and CI will tell you if you have to fix anything".

[Eric Wieser]

Of course, it's often a good plan to discuss the idea first as you are doing in this thread; there's no point fixing CI if the consensus from review is that it's not a good change!