instRing

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.instRing

English

If k is a Ring and G a Monoid with a MulSemiringAction, SkewMonoidAlgebra k G forms a Ring.

Русский

Если k — кольцо и G — моноид с действием, SkewMonoidAlgebra k G образует кольцо.

LaTeX

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

Lean4

instance instRing [Ring k] [Monoid G] [MulSemiringAction G k] : Ring (SkewMonoidAlgebra k G)
    where
  __ := instNonAssocRing
  __ := instSemiring

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru