rid_symm_apply — Mathlib

English

The lift preserves addition and is linear over the base ring; in particular, lift respects tmul structure.

Русский

Лифт сохраняет сложение и линейность по базовому кольцу; в частности, лифт сохраняет структуру tmul.

LaTeX

$$$\\text{lift}(f,g,hfg)\\; (x + y) = \\text{lift}(f,g,hfg)(x) + \\text{lift}(f,g,hfg)(y).$$$

Lean4

@[simp]
theorem rid_symm_apply (a : A) : (TensorProduct.rid R S A).symm a = a ⊗ₜ 1 :=
  rfl

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