[Merged by Bors] - chore(field_theory/splitting_field): refactor `splitting_field`

[riccardobrasca]

We refactor the definition of splitting_field. The main motivation is to backport !4#4891 since the is seems very problematic to port the current design.

Zulip discussion relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField

---

All the modifications not in field_theory.splitting_field.construction have been done to solve timeouts.

• [x] depends on: #19179

• [x] depends on: #19187

• [x] depends on: #19184

• leanprover-community/mathlib4#4891

[eric-wieser]

Just to note I back-ported a more bikesheddy side of 4891 in #19179

[riccardobrasca]

~The linter will complain and there is some doc to be fixed. I will fix everything tomorrow.~ Done.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib#19179
• leanprover-community/mathlib#19187
• leanprover-community/mathlib#19184 By Dependent Issues (🤖). Happy coding!

[ericrbg]

Why do we have to disable the instances now? Is it just a timeout if the instance is kept in, or an actual diamond? I like the solution, though, not the most elegant but definitely a good way to essentially copy a field construction

[riccardobrasca]

Why do we have to disable the instances now? Is it just a timeout if the instance is kept in, or an actual diamond? I like the solution, though, not the most elegant but definitely a good way to essentially copy a field construction

It's causing a timeout, but I am not sure why. I can have a look tomorrow. splitting_field.algebra' is the instance giving the algebra structure over A, where K is an A-algebra: maybe it is a loop?

I don't think there can be a diamond with the K-algebra structure, the definition is the same:

instance algebra : algebra K (splitting_field f) :=
ideal.quotient.algebra _

instance algebra' {R : Type*} [comm_semiring R] [algebra R K] : algebra R (splitting_field f) :=
ideal.quotient.algebra _

Indeed

example : splitting_field.algebra f = @splitting_field.algebra' K _ f K _ (algebra.id K) := rfl

works. Maybe there another instance algebra (znmod p) (znmod p)?

[jcommelin]

Thanks :tada:

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests