mul_right_eq_zero_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_right_eq_zero_iff (h : Monic p) {q : R[X]} : p * q = 0 ↔ q = 0 := by
  by_cases hq : q = 0 <;> simp [h.mul_right_ne_zero, hq]

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