lmul'_comp_includeRight — Mathlib

English

Let R be a commutative semiring and S an R-algebra. The left multiplication map, composed with the right inclusion, is the identity on R → S.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lmul'_comp_includeRight : (lmul' R : _ →ₐ[R] S).comp includeRight = AlgHom.id R S :=
  AlgHom.ext <| one_mul

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