English
If S is compatible for SMul with itself over R (i.e., CompatibleSMul R S S S holds), then the left-multiplication construction lmulEquiv provides an isomorphism of algebras S ⊗_R S ≅_S S.
Русский
Если умножение элементов S совместимо с самим собой над R (условие CompatibleSMul), то отображение lmulEquiv даёт изоморфизм S ⊗_R S ≅_S S.
LaTeX
$$$ S \otimes_R S \cong_S S \quad (\text{via } lmulEquiv) $$$
Lean4
/-- If multiplication by elements of S can switch between the two factors of `S ⊗[R] S`,
then `lmul''` is an isomorphism. -/
def lmulEquiv [CompatibleSMul R S S S] : S ⊗[R] S ≃ₐ[S] S :=
.ofAlgHom (lmul'' R) includeLeft lmul'_comp_includeLeft <|
AlgHom.ext fun x ↦
x.induction_on (by simp)
(fun x y ↦ show (x * y) ⊗ₜ[R] 1 = x ⊗ₜ[R] y by rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one])
fun _ _ hx hy ↦ by simp_all [add_tmul]
