refactor: Add invariants theorem for Higgs potential

[jstoobysmith]

Adding the theorem which says that the Higgs potential is the most general potential up to order 4 which is invariant under the SM action.

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[morrison-daniel]

Can't give a full review yet, but I think some of this should be separated into other lemmas. For example, define V' and p' in general and then pretty much each of your have statements can be its own lemma.

[jstoobysmith]

@morrison-daniel I did something similar to this. I have defined a more general notion of an EffectivePotential and then define properties of that, the proof is slightly different from what I had before, but hopefully it is now slightly more generalizable.