feat(Algebra/Polynomial/Lifts): every polynomial lifts along a surjective ring homomorphism (leanprover-community#38708)

This PR adds a lemma stating that every polynomial lifts along a surjective ring homomorphism (this could also be phrased as `lifts_eq_top`, but in practice it's membership in lifts that unlocks all of the API for `lifts`).

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Algebra/Polynomial/Lifts.lean

@@ -85,6 +85,9 @@ theorem lifts_iff_coeffs_subset_range (p : S[X]) :
     · exact ⟨0, by simp [hn]⟩
     · exact h <| coeff_mem_coeffs hn
 
+theorem mem_lifts_of_surjective (hf : Function.Surjective f) (p : S[X]) : p ∈ lifts f :=
+  (lifts_iff_coeff_lifts p).mpr fun n ↦ hf (p.coeff n)
+
 /-- If `(r : R)`, then `C (f r)` lifts. -/
 theorem C_mem_lifts (f : R →+* S) (r : R) : C (f r) ∈ lifts f :=
   ⟨C r, by