instNonUnitalRing — Mathlib

English

If k is a Ring and sets as above, SkewMonoidAlgebra k G inherits a NonAssocRing structure.

Русский

Если k — кольцо и условия выполнены, SkewMonoidAlgebra k G наследует структуру NonAssocRing.

LaTeX

$$$ \text{NonAssocRing}(SkewMonoidAlgebra k G) $$$

Lean4

instance instNonUnitalRing [Ring k] [Monoid G] [MulSemiringAction G k] : NonUnitalRing (SkewMonoidAlgebra k G)
    where
  __ := instAddCommGroup
  __ := instNonUnitalSemiring

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