R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ AlgHom.range (toAdjoin R x)
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Function.Surjective ↑(toAdjoin R x)
rw [← range_top_iff_surjective, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ ↑(AlgHom.range (toAdjoin R x))
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ AlgHom.range (toAdjoin R x)
refine' adjoin_le _
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ Set.range ↑(toAdjoin R x)
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ ↑(AlgHom.range (toAdjoin R x))
simp only [AlgHom.coe_range, Set.mem_range]
case mk
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y₁ : S
y₂ : y₁ ∈ ↑(adjoin R {x})
h : { val := y₁, property := y₂ } ∈ Subtype.val ⁻¹' {x}
⊢ { val := y₁, property := y₂ } ∈ Set.range ↑(toAdjoin R x)
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ Set.range ↑(toAdjoin R x)
rintro ⟨y₁, y₂⟩ h
no goals
case mk
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y₁ : S
y₂ : y₁ ∈ ↑(adjoin R {x})
h : { val := y₁, property := y₂ } ∈ Subtype.val ⁻¹' {x}
⊢ { val := y₁, property := y₂ } ∈ Set.range ↑(toAdjoin R x)
refine' ⟨mk (minpoly R x) X, by simpa [toAdjoin] using h.symm⟩
no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y₁ : S
y₂ : y₁ ∈ ↑(adjoin R {x})
h : { val := y₁, property := y₂ } ∈ Subtype.val ⁻¹' {x}
⊢ ↑(toAdjoin R x) (↑(mk (minpoly R x)) X) = { val := y₁, property := y₂ }
simpa [toAdjoin] using h.symm