instSemiring — Mathlib

English

If α is a semiring and α is small, then Shrink α carries a semiring structure transported via the natural equivalence Shrink α ≃ α.

Русский

Если α — полукольцо и α является малым типом, то Shrink α обладает структурой полукольца, перенесенной через естественное эквивалентное отображение Shrink α ≃ α.

LaTeX

$$$(\text{Semiring } \alpha \land \text{Small } \alpha) \Rightarrow \text{Semiring}(\text{Shrink } \alpha)$$$

Lean4

instance [Semiring α] : Semiring (Shrink.{v} α) :=
  (equivShrink α).symm.semiring

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