splits_of_map_eq_C — Mathlib

English

If f maps to a constant, Splits holds.

Русский

Если образ полинома по i является константой, то выполняется распад.

LaTeX

$$Splits i f := (f.map i) = C a or ∀ {g}, Irreducible g → g ∣ f.map i → degree g = 1$$

Lean4

theorem splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : Splits i f :=
  letI := Classical.decEq L
  if ha : a = 0 then Or.inl (h.trans (ha.symm ▸ C_0))
  else
    Or.inr fun hg ⟨p, hp⟩ =>
      absurd hg.1 <|
        Classical.not_not.2 <|
          isUnit_iff_degree_eq_zero.2 <| by
            have := congr_arg degree hp
            rw [h, degree_C ha, degree_mul, @eq_comm (WithBot ℕ) 0, Nat.WithBot.add_eq_zero_iff] at this
            exact this.1

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