one_mul — Mathlib

English

For any x in the PiTensorProduct, mul x (tprod R 1) = x, i.e., 1 acts as a multiplicative unit.

Русский

Для любого x из PiTensorProduct выполняется mul x (tprod R 1) = x, то есть 1 является тензорной единицей.

LaTeX

$$$mul\\ x\\ (tprod\\ R\\ 1) = x$$$

Lean4

protected theorem one_mul (x : ⨂[R] i, A i) : mul (tprod R 1) x = x := by
  induction x using PiTensorProduct.induction_on with
  | smul_tprod => simp
  | add _ _ h1 h2 => simp [map_add, h1, h2]

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