mul_right_ne_zero — Mathlib

English

If p is monic and q ≠ 0, then p · q ≠ 0.

Русский

Если p мононичен и q ≠ 0, то p·q ≠ 0.

LaTeX

$$$\forall {R} [\text{Semiring } R] {p : Polynomial R} (hp : Monic p) {q : Polynomial R} (hq : q \neq 0), p * q \neq 0$$$

Lean4

theorem mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q ≠ 0 :=
  by
  by_cases h : p = 1
  · simpa [h]
  rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
  refine ⟨hq, ?_⟩
  rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
  refine (lt_trans ?_ h).ne'
  simp

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