coeffIntegerNormalization_of_coeff_zero

English

If the i-th coefficient of p is zero, then coeffIntegerNormalization M p i is zero.

Русский

Если i-й коэффициент p равен нулю, то coeffIntegerNormalization M p i равен нулю.

LaTeX

$$$p(i) = 0 \Rightarrow \ text{coeffIntegerNormalization }(M,p,i) = 0$$$

Lean4

theorem coeffIntegerNormalization_of_coeff_zero (p : S[X]) (i : ℕ) (h : coeff p i = 0) :
    coeffIntegerNormalization M p i = 0 := by
  simp only [coeffIntegerNormalization, h, mem_support_iff, not_true, Ne, dif_neg, not_false_iff]

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