# Commit 2024-09-04 10:38 1b14d3d6

View on Github →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`

.