mul_left_ne_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_left_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p ≠ 0 :=
  by
  by_cases h : p = 1
  · simpa [h]
  rw [Ne, ← degree_eq_bot, 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

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