nonAssocRing — Mathlib

English

The structure MonoidAlgebra R M forms a nonassociative ring when M is a MulOneClass monoid; associativity is not assumed or required for the multiplication.

Русский

Структура MonoidAlgebra R M образует неассоциативное кольцо, если M — моноид MulOneClass; ассоциативность умножения не требуется.

LaTeX

$$$\\mathrm{NonAssocRing}(\\mathrm{MonoidAlgebra}(R,M)).$$$

Lean4

@[to_additive (dont_translate := R)]
instance nonAssocRing [MulOneClass M] : NonAssocRing (MonoidAlgebra R M)
    where
  intCast z := single 1 z
  intCast_ofNat n := by simp [natCast_def]
  intCast_negSucc n := by simp [natCast_def, one_def]

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