algebraMap_eq_inl_comp — Mathlib

English

Under appropriate hypotheses, Unitization(R, A) is a semiring, combining additive and multiplicative structures coherently.

Русский

При соответствующих предположениях Unitization(R, A) является полугруппой-колцем, где сложение и умножение согласованы.

LaTeX

$$$\text{Semiring}(\mathrm{Unitization}(R,A))$$$

Lean4

theorem algebraMap_eq_inl_comp : ⇑(algebraMap S (Unitization R A)) = inl ∘ algebraMap S R :=
  rfl

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