optionEquivLeft_C — Mathlib

English

The action of optionEquivLeft on a constant C r equals Polynomial C r in the underlying polynomial ring.

Русский

Действие optionEquivLeft на константу C r даёт Polynomial C r в базовом кольцевом кольце.

LaTeX

$$$\text{optionEquivLeft} \;R\;S_1\; (C r) = \text{Polynomial} (C r)$$$

Lean4

theorem optionEquivLeft_C (r : R) : optionEquivLeft R S₁ (C r) = Polynomial.C (C r) := by
  simp only [optionEquivLeft_apply, aeval_C, Polynomial.algebraMap_apply, algebraMap_eq]

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