isUnit_leadingCoeff_mul_left_eq_zero_iff

English

If the leading coefficient of p is a unit, then q · p = 0 if and only if q = 0, for all q ∈ R[X].

Русский

Если ведущий коэффициент p является единицей, то ∀q ∈ R[X], q p = 0 ⇔ q = 0.

LaTeX

$$$\operatorname{lc}(p) \in R^{\times} \Rightarrow (q \cdot p = 0) \iff (q = 0) \quad (\forall q \in R[X]).$$$

Lean4

theorem isUnit_leadingCoeff_mul_left_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} : q * p = 0 ↔ q = 0 :=
  by
  constructor
  · intro hp
    replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
    simp only [zero_mul] at hp
    rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
    refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    simp
  · rintro rfl
    rw [zero_mul]

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