rid — Mathlib

English

Another presentation of lid_tmul: lid R S A (r ⊗ a) = r • a.

Русский

Ещё одно выражение lid_tmul: lid (r ⊗ a) = r · a.

LaTeX

$$$\\mathrm{lid\\_tmul}\\; (r \\in R)\\ (a \\in A):\\; \\mathrm{TensorProduct.lid}\\; R\\; S\\; A\\; (r \\otimes_T\\; a) = r \\cdot a.$$$

Lean4

/-- The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism.

Note that if `A` is commutative this can be instantiated with `S = A`.
-/
protected nonrec def rid : A ⊗[R] R ≃ₐ[S] A :=
  algEquivOfLinearEquivTensorProduct (AlgebraTensorModule.rid R S A)
    (fun a₁ a₂ r₁ r₂ => smul_mul_smul_comm r₁ a₁ r₂ a₂ |>.symm) (one_smul R _)

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