R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : A), x ∈ S → _root_.IsAlgebraic R x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ IsAlgebraic S ↔ Algebra.IsAlgebraic R { x // x ∈ S }
delta Algebra.IsAlgebraic Subalgebra.IsAlgebraic
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : { a // a ∈ S }), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : A), x ∈ S → _root_.IsAlgebraic R x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
rw [Subtype.forall']
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : { a // a ∈ S }), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : { x // x ∈ S }), _root_.IsAlgebraic R x
refine' forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl _
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
have h : Function.Injective S.val := Subtype.val_injective
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(val S) (↑(aeval x) p) = 0
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(aeval x) p = 0
conv_rhs => rw [← h.eq_iff, AlgHom.map_zero]
no goals
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : { a // a ∈ S }
p : R[X]
h : Function.Injective ↑(val S)
⊢ ↑(aeval ↑x) p = 0 ↔ ↑(val S) (↑(aeval x) p) = 0
rw [← aeval_algHom_apply, S.val_apply]