toFunLinear_mul_tmul_mul_aux_1 — Mathlib

English

For a polynomial p, index k, and a ∈ A, the conditional expression that selects either a·algebraMap(coeff p k) or 0 evaluates to a·algebraMap(coeff p k).

Русский

Для полинома p, индекса k и элемента a ∈ A выражение с условием, выбирающее между a·algebraMap(coeff p k) и 0, равно a·algebraMap(coeff p k).

LaTeX

$$$\\mathrm{ite}(coeff(p,k) \\neq 0)\,(a \\cdot (\\mathrm{algebraMap}\,R\,A(\,coeff(p,k)\\,)))\\ 0 = a \\cdot (\\mathrm{algebraMap}\,R\,A( coeff(p,k) ))$$$

Lean4

theorem toFunLinear_mul_tmul_mul_aux_1 (p : R[X]) (k : ℕ) (h : Decidable ¬p.coeff k = 0) (a : A) :
    ite (¬coeff p k = 0) (a * (algebraMap R A) (coeff p k)) 0 = a * (algebraMap R A) (coeff p k) := by
  classical split_ifs <;> simp [*]

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