lmul'_comp_includeLeft — Mathlib

English

Let R be a commutative semiring and S an R-algebra. The left multiplication map, viewed as an R-algebra hom, composed with the natural inclusion of R into the tensor product, equals the identity map R → S.

Русский

Пусть $R$ — коммутативное полукольцо, $S$ — алгебра над $R$. Тогда гомоморфизм левого умножения, воспринимаемый как алгебраический гомоморфизм, в композиции с естественным включением $R$ в тензорное произведение, даёт тождественный отображение $R o S$.

LaTeX

$$$ (lmul' \, R) \circ includeLeft = \mathrm{id}_{R \to S} $$

Lean4

@[simp]
theorem lmul'_comp_includeLeft : (lmul' R : _ →ₐ[R] S).comp includeLeft = AlgHom.id R S :=
  AlgHom.ext <| mul_one

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