toFunLinear_one_tmul_one

Mathlib.RingTheory.PolynomialAlgebra

URI: https://scilib.ai/kg/mathlib#PolyEquivTensor.toFunLinear_one_tmul_one

← MathLib Explorer

English

The image of 1 ⊗ 1 under toFunLinear is the constant polynomial 1.

Русский

Изображение 1 ⊗ 1 подtoFunLinear равно константному полиномy 1.

LaTeX

$$$(toFunLinear_R A)(1 \\otimes 1) = 1$$

Lean4

theorem toFunLinear_one_tmul_one : toFunLinear R A (1 ⊗ₜ[R] 1) = 1 := by
  rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru