isUnit_leadingCoeff_mul_right_eq_zero_iff

English

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

Русский

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

LaTeX

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

Lean4

theorem isUnit_leadingCoeff_mul_right_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} : p * q = 0 ↔ q = 0 :=
  by
  constructor
  · intro hp
    rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
    have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
    rwa [this, Monic.mul_right_eq_zero_iff] at hp
    exact monic_of_isUnit_leadingCoeff_inv_smul _
  · rintro rfl
    simp

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