comp_C_mul_X_eq_zero_iff — Mathlib

English

Let hr be a member of nonZeroDivisors R. Then p.comp (C r · X) = 0 if and only if p = 0.

Русский

Пусть hr ∈ nonZeroDivisors R. Тогда p.comp (C r · X) = 0 тогда и только тогда, когда p = 0.

LaTeX

$$$p.comp (C\\ r * X) = 0 \\iff p = 0 \\quad (r \\in nonZeroDivisors R)$$$

Lean4

theorem comp_C_mul_X_eq_zero_iff {r : R} (hr : r ∈ nonZeroDivisors R) : p.comp (C r * X) = 0 ↔ p = 0 :=
  by
  simp_rw [ext_iff]
  refine forall_congr' fun n ↦ ?_
  rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]

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