Say I want to formalize a proposition that talks about rings of multivariate polynomials in Isabelle.
A related AFP entry seems to be:
https://www.isa-afp.org/entries/Polynomials.html
However, in the Isabelle distribution I only find:
HOL/Algebra/Polynomials.thy
which seems to only deal with univariate polynomials. According to `find_theorems` in the AFP I deduce I have to download the AFP entry and import it from some directory in my machine. This in turn implies repeating the process for all the dependencies of the AFP entry.
Is this the correct/most efficient way to go?
Yes. To use the results of any theory in Isabelle you have to process it and its dependencies.
For the AFP, it is usually simplest to download the entire archive and import the theory you want. Isabelle will then only process the ones it depends on, not the entire archive, i.e. it will do the dependency resolution for you.
(See also the docs on the AFP website on using another AFP entry for how to make sure Isabelle sees looks in the AFP for dependencies once you have downloaded it).