F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : ∀ (j : ι), j ∈ insert a t → Splits i (s j)
⊢ Splits i (∏ x in insert a t, s x)
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
refine' Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => _
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (∏ x in insert a t, s x)
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : ∀ (j : ι), j ∈ insert a t → Splits i (s j)
⊢ Splits i (∏ x in insert a t, s x)
rw [Finset.forall_mem_insert] at ht
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (s a * ∏ x in t, s x)
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (∏ x in insert a t, s x)
rw [Finset.prod_insert hat]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (s a * ∏ x in t, s x)
exact splits_mul i ht.1 (ih ht.2)