tprodCoeff_eq_smul_tprod

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.tprodCoeff_eq_smul_tprod

← MathLib Explorer

English

For any z in R and any f, tprodCoeff R z f = z • tprod R f.

Русский

Для любого z в R и любого f выполняется tprodCoeff R z f = z • tprod R f.

LaTeX

$$$$ tprodCoeff(R,z,f) = z \cdot tprod(R,f) $$$$

Lean4

@[simp]
theorem tprodCoeff_eq_smul_tprod (z : R) (f : Π i, s i) : tprodCoeff R z f = z • tprod R f :=
  by
  have : z = z • (1 : R) := by simp only [mul_one, Algebra.id.smul_eq_mul]
  conv_lhs => rw [this]
  rfl

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

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

Разделы

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

Аффилиация

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