splits_of_degree_le_one — Mathlib

English

If degree f ≤ 1 then Splits i f.

Русский

Если deg f ≤ 1, то Splits i f.

LaTeX

$$degree f ≤ 1 → Splits i f$$

Lean4

theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
  if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
  else by
    push_neg at hif
    rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.orderSucc_coe, Nat.succ_eq_succ] at hif
    exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)

Похожие утверждения