lid — Mathlib

English

The base ring R is a right identity for A under the tensor product, up to an algebra isomorphism.

Русский

Базовое кольцо R является правой идентичностью для A в тензорном произведении, до алгебраического изоморфизма.

LaTeX

$$$(\\mathrm{lid}\\, R\\, A)(r \\otimes a) = r \\cdot a.$$$

Lean4

/-- The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism.
-/
protected nonrec def lid : R ⊗[R] A ≃ₐ[R] A :=
  algEquivOfLinearEquivTensorProduct (TensorProduct.lid R A)
    (by
      simp only [mul_smul, lid_tmul, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
      simp_rw [← mul_smul, mul_comm]
      simp)
    (by simp [Algebra.smul_def])

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