mul_one

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.mul_one

English

Multiplication on A ⊗_R B is associative: (xy)z = x(yz) for all x,y,z.

Русский

Умножение на A ⊗_R B ассоциативно: (xy)z = x(yz).

LaTeX

$$$ \text{mul}(\text{mul}(x,y), z) = \text{mul}(x, \text{mul}(y,z)) $$$

Lean4

protected theorem mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

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

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

Разделы

Аффилиация

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