feat(ring_theory/algebraic): is_algebraic_iff_not_injective (#9254)

leanprover-community · Sep 23, 2021 · ea59c90 · ea59c90
1 parent 9e367ff
commit ea59c90
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/ring_theory/algebraic.lean b/src/ring_theory/algebraic.lean
@@ -65,6 +65,10 @@ begin
   simp only [algebra.mem_top, forall_prop_of_true, iff_self],
 end
 
+lemma is_algebraic_iff_not_injective {x : A} : is_algebraic R x ↔ 
+  ¬ function.injective (polynomial.aeval x : polynomial R →ₐ[R] A) :=
+by simp only [is_algebraic, alg_hom.injective_iff, not_forall, and.comm, exists_prop]
+
 end
 
 section zero_ne_one