Commit 2025-06-28 11:35 490148fe

refactor(RingTheory/RingHom): factor out proofs for Algebra.FiniteType (#22931) The current way to use locality of a given property of algebras is to convert everything into the language of RingHoms and then for example the RingHom.OfLocalizationSpanTarget API. This has two disadvantages:

1. The ring hom property API fixes the universes of source and target to be the same, hence we unnecessarily lose out on some universe generality.
2. The results for RingHoms are proven by translating everything in terms of Algebra, so we duplicate the translation steps. This PR refactors RingHom.FiniteType to do all locality proofs in the language of Algebras and translate it into the corresponding RingHom.OfLocalizationSpan{Target} in the last step. We also streamline some of the translation proofs by unifying the API.