lifts_and_natDegree_eq_and_monic — Mathlib

English

If p lifts and p is monic, then there exists q with map f q = p, q.natDegree = p.natDegree, and q.Monic.

Русский

Если p поднимается и моничный, тогда существует q такой, что map f q = p, q.natDegree = p.natDegree и q.Monic.

LaTeX

$$$ \exists q : R[X], map f q = p \land q.natDegree = p.natDegree \land q.Monic$$$

Lean4

theorem lifts_and_natDegree_eq_and_monic {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) :
    ∃ q : R[X], map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic :=
  by
  rcases subsingleton_or_nontrivial S with hR | hR
  · obtain rfl : p = 1 := Subsingleton.elim _ _
    exact ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
  obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
  exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

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