instNonUnitalNonAssocRing — Mathlib

English

If k is a Ring and G a Monoid acting on k byMul, then SkewMonoidAlgebra k G is a NonUnitalNonAssocRing.

Русский

Если k — кольцо и G — моноид, действующий на k, то SkewMonoidAlgebra k G является NonUnitalNonAssocRing.

LaTeX

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

Lean4

instance instNonUnitalNonAssocRing [Ring k] [Monoid G] [MulSemiringAction G k] :
    NonUnitalNonAssocRing (SkewMonoidAlgebra k G)
    where
  __ := instAddCommGroup
  __ := instNonUnitalNonAssocSemiring

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