F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif : 0 < degree (map i f)
⊢ Splits i f
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif : ¬degree (map i f) ≤ 0
⊢ Splits i f
push_neg at hif
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif✝ : 0 < degree (map i f)
hif : ↑(Nat.succ 0) ≤ degree (map i f)
⊢ Splits i f
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif : 0 < degree (map i f)
⊢ Splits i f
rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.succ_coe, Nat.succ_eq_succ] at hif
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif✝ : 0 < degree (map i f)
hif : ↑(Nat.succ 0) ≤ degree (map i f)
⊢ Splits i f
exact splits_of_map_degree_eq_one i (le_antisymm ((degree_map_le i _).trans hf) hif)