mul_natDegree_lt_iff — Mathlib

English

For a monic p, (p · q).natDegree < p.natDegree iff p ≠ 1 and q = 0.

Русский

Для мононичного p, (p · q).natDegree < p.natDegree тогда и только если p ≠ 1 и q = 0.

LaTeX

$$$\forall {R} [\text{Semiring } R] {p : Polynomial R}, p.Monic \rightarrow \forall {q : Polynomial R}, \operatorname{natDegree} (p * q) < \operatorname{natDegree} p \iff (p \neq 1) \land (q = 0)$$$

Lean4

theorem mul_natDegree_lt_iff (h : Monic p) {q : R[X]} : (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0 :=
  by
  by_cases hq : q = 0
  · suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
    exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
  · simp [h.natDegree_mul', hq]

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