contract_add — Mathlib

English

If p ≠ 0, contraction by p is additive: contraction distributes over addition: contract_p(f+g) = contract_p(f) + contract_p(g).

Русский

Если p ≠ 0, сжатие по p является аддитивным: contract_p(f+g) = contract_p(f) + contract_p(g).

LaTeX

$$$$\mathrm{contract}_p(f+g)=\mathrm{contract}_p(f)+\mathrm{contract}_p(g)$$$$

Lean4

theorem contract_add {p : ℕ} (hp : p ≠ 0) (f g : R[X]) : contract p (f + g) = contract p f + contract p g := by ext;
  simp_rw [coeff_add, coeff_contract hp, coeff_add]

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