feat(Algebra/Polynomial/Eval/Subring): notMem_map_range (leanprover-community#36108)

A "not" version of `mem_map_range`.

Author: justus-springer

Mathlib/Algebra/Polynomial/Eval/Subring.lean

@@ -43,8 +43,15 @@ theorem mem_map_rangeS {p : S[X]} : p ∈ (mapRingHom f).rangeS ↔ ∀ n, p.coe
     use C c * X ^ i
     rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
 
+theorem notMem_map_rangeS {p : S[X]} : p ∉ (mapRingHom f).rangeS ↔ ∃ n, p.coeff n ∉ f.rangeS :=
+  (mem_map_rangeS f (p := p)).not.trans not_forall
+
 theorem mem_map_range {R S : Type*} [Ring R] [Ring S] (f : R →+* S) {p : S[X]} :
     p ∈ (mapRingHom f).range ↔ ∀ n, p.coeff n ∈ f.range :=
   mem_map_rangeS f
 
+theorem notMem_map_range {R S : Type*} [Ring R] [Ring S] (f : R →+* S) {p : S[X]} :
+    p ∉ (mapRingHom f).range ↔ ∃ n, p.coeff n ∉ f.range :=
+  notMem_map_rangeS f
+
 end Polynomial