mathlib
b353176c - feat(field_theory/splitting_field): fix the diamond (#18857)

Commit
2 years ago
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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Author
Parents
Loading