no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ IsAlgebraic R x ↔ ¬Function.Injective ↑(aeval x)
simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]