contract_expand — Mathlib

English

Contraction is a left inverse of expansion: contract p (expand R p f) = f when p ≠ 0.

Русский

Контракт после расширения является обратной связью слева: contract p (expand R p f) = f при p ≠ 0.

LaTeX

$$$\operatorname{contract}(p, \operatorname{expand}(R,p,f)) = f \quad(\text{при } p \neq 0)$$$

Lean4

theorem contract_expand {f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f :=
  by
  ext
  simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]

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