R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ (∀ (x : A), _root_.IsAlgebraic R x) ↔ ∀ (x : A), x ∈ ⊤ → _root_.IsAlgebraic R x
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ IsAlgebraic R A ↔ Subalgebra.IsAlgebraic ⊤
delta Algebra.IsAlgebraic Subalgebra.IsAlgebraic
no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ (∀ (x : A), _root_.IsAlgebraic R x) ↔ ∀ (x : A), x ∈ ⊤ → _root_.IsAlgebraic R x
simp only [Algebra.mem_top, forall_prop_of_true, iff_self_iff]