subsemiring — Mathlib

English

The canonical algebra isomorphism between the direct sum and R is given by mapping each homogeneous component to its corresponding element in R.

Русский

Каноническое алгебра-изоморфизм DirectSum в R отправляет каждую однородную компоненту в соответствующий элемент в R.

LaTeX

$$$$ DirectSum.coeAlgHom(A) : (⨁ i, A_i) \cong_S R. $$$$

Lean4

/-- The subsemiring `A 0` of `R`. -/
def subsemiring : Subsemiring R where
  carrier := A 0
  __ := submonoid A
  add_mem' := add_mem
  zero_mem' :=
    zero_mem
      (A 0)
        -- TODO: it might be expensive to unify `A` in this instance in practice

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