polyEquivTensor_apply — Mathlib

English

For any p ∈ A[X], the value of polyEquivTensor R A p equals p evaluated by includeLeft and X.

Русский

Для любого p ∈ A[X], значение polyEquivTensor R A p равно p, вычисленному через includeLeft и X.

LaTeX

$$polyEquivTensor_R A p = p.eval₂(includeLeft, (1) ⊗ X)$$

Lean4

@[simp]
theorem polyEquivTensor_apply (p : A[X]) :
    polyEquivTensor R A p = p.eval₂ (includeLeft : A →ₐ[R] A ⊗[R] R[X]) ((1 : A) ⊗ₜ[R] (X : R[X])) :=
  rfl

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