R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p✝ q : R[X]
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p✝ q : R[X]
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (↑f) (rootSet p S) (rootSet p S')
refine' rootSet_maps_to' (fun h₀ => _) f
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p q : R[X]
inst✝⁷ : CommRing T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') 0 = 0
⊢ map (algebraMap T S) 0 = 0
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p✝ q : R[X]
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0
obtain rfl : p = 0 :=
  map_injective _ (NoZeroSMulDivisors.algebraMap_injective T S') (by rwa [Polynomial.map_zero])
no goals
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p q : R[X]
inst✝⁷ : CommRing T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') 0 = 0
⊢ map (algebraMap T S) 0 = 0
exact Polynomial.map_zero _
no goals
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
p✝ q : R[X]
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S') p = map (algebraMap T S') 0
rwa [Polynomial.map_zero]