Commit 2024-09-04 10:38 1b14d3d6

feat(ModelTheory): Lefschetz principle for AlgClosed Fields (#6617) The main question here was how to integrate the model theoretic classes with the normal type classes. The solution was the CompatibleRing class, and to apply a theorem about the model theory of Alg Closed Fields to a literal Alg Closed field, all you have to do is letI := compatibleRingOfRing K. Everything else can then be done by type class search. Going the other way, from a model theoretic field to a normal field is a bit more difficult, but I think people will do this more rarely, particularly with a complete theory like ACF p.