instCommSemiringObjForget — Mathlib

English

For any commutative semiring R, the forgetful image (forget₂ CommSemiRingCat → SemiRingCat).obj R carries a canonical commutative semiring structure on its underlying carrier, i.e., forgetting the commutativity preserves a semiring structure on the same carrier.

Русский

Для любого коммутативного полукольца R носитель, который получается при забывании, на базовом носителе несёт каноническую структуру коммутативного полукольца; забывание сохраняет структуру полукольца на том же носителе.

LaTeX

$$$\operatorname{CommSemiring}\big((\operatorname{forget CommSemiRingCat})\! .\!\obj R\big) \text{ is defined by the same carrier as } R$,$$

Lean4

instance {R : CommSemiRingCat} : CommSemiring ((forget CommSemiRingCat).obj R) :=
  (inferInstance : CommSemiring R.carrier)

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