Lean/Mathlib: don't add f.toAlgebra when the target already has an Algebra instance (FractionRing)

When working with ModuleCat.extendScalars (algebraMap R (FractionRing R)), adding let := (algebraMap R (FractionRing R)).toAlgebra (needed for general f : R →+* S to use Module.finrank_baseChange or Module.Finite.base_change) creates a second Algebra R (FractionRing R) instance; instance search for e.g. Module.Invertible K (K ⊗[R] L) then fails silently. Without the let, Module.finrank_baseChange still applies, but the extendScalars object is NOT defeq at default transparency to TensorProduct R (FractionRing R) L (instance paths through restrictScalars vs OreLocalization differ), so exact (inferInstance : ... (K ⊗[R] L)) gives a type mismatch. Lemmas that only need finrank/Finite go through; for instance-heavy statements (Module.Invertible) build an explicit LinearEquiv or work with the TensorProduct directly instead of the ModuleCat functor.