F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i f * map i g✝
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i (f * g✝)
rw [Polynomial.map_mul]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i f * map i g✝
exact hg.trans (dvd_mul_right _ _)
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i f * map i g✝
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i (f * g✝)
rw [Polynomial.map_mul]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i f * map i g✝
exact hg.trans (dvd_mul_left _ _)