chore(Mathlib/Algebra/Polynomial/Splits.lean): automated extraction (#39238)

This PR was automatically created from PR #28013 by @astrainfinita via a [review comment](#28013 (comment)) by @jcommelin.

Co-authored-by: astrainfinita <19634778+astrainfinita@users.noreply.github.com>

Author: mathlib-splicebot[bot]

Mathlib/Algebra/Polynomial/Splits.lean

@@ -537,6 +537,11 @@ section
 variable {A B : Type*} [CommRing R] [Field A] [Algebra R A]
   [CommRing B] [IsDomain B] [Algebra R B] {f : R[X]}
 
+theorem Splits.map_aroots_algebraMap [Algebra A B] [IsScalarTower R A B]
+    (hf : (f.map (algebraMap R A)).Splits) :
+    (f.aroots A).map (algebraMap A B) = f.aroots B := by
+  rw [← aroots_map B A, aroots, aroots, hf.roots_map]
+
 theorem Splits.image_rootSet (hf : (f.map (algebraMap R A)).Splits)
     (g : A →ₐ[R] B) : g '' f.rootSet A = f.rootSet B := by
   classical