R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
⊢ ↑(aeval s) (primPart p) = 0
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(aeval s) p = 0
⊢ ↑(aeval s) (primPart p) = 0
rw [eq_C_content_mul_primPart p, map_mul, aeval_C] at hp
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : content p ≠ 0
⊢ ↑(aeval s) (primPart p) = 0
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
⊢ ↑(aeval s) (primPart p) = 0
have hcont : p.content ≠ 0 := fun h => hpzero (content_eq_zero_iff.1 h)
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : ↑(algebraMap R S) (content p) ≠ ↑(algebraMap R S) 0
⊢ ↑(aeval s) (primPart p) = 0
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : content p ≠ 0
⊢ ↑(aeval s) (primPart p) = 0
replace hcont := Function.Injective.ne (NoZeroSMulDivisors.algebraMap_injective R S) hcont
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : ↑(algebraMap R S) (content p) ≠ 0
⊢ ↑(aeval s) (primPart p) = 0
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : ↑(algebraMap R S) (content p) ≠ ↑(algebraMap R S) 0
⊢ ↑(aeval s) (primPart p) = 0
rw [map_zero] at hcont
no goals
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_1
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : NoZeroSMulDivisors R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : ↑(algebraMap R S) (content p) * ↑(aeval s) (primPart p) = 0
hcont : ↑(algebraMap R S) (content p) ≠ 0
⊢ ↑(aeval s) (primPart p) = 0
exact eq_zero_of_ne_zero_of_mul_left_eq_zero hcont hp