Commit 2023-05-22 12:50 b353176c

feat(field_theory/splitting_field): fix the diamond (#18857) This re-implements how instances for splitting_field in such a way that we can now avoid diamonds with the N, Z and Q-actions. This makes a lot more instances safe, which is good for e.g. flt-regular. Many thanks to @Vierkantor for many of the ideas and all the distrib_smul PRs that were needed for this.