nonAssocSemiring — Mathlib

English

There is a natural embedding of M into MonoidAlgebra R M given by a ↦ single a 1; this defines a monoid homomorphism

Русский

Существует естественное вложение M в MonoidAlgebra R M, задаваемое a ↦ single a 1; это образует гомоморфизм моноидов.

LaTeX

$$$\forall a,b \in M,\; \operatorname{of}(a b) = \operatorname{of}(a) * \operatorname{of}(b)$$$

Lean4

@[to_additive (dont_translate := R)]
instance nonAssocSemiring : NonAssocSemiring (MonoidAlgebra R M)
    where
  natCast n := single 1 n
  natCast_zero := by simp
  natCast_succ := by simp [one_def]
  one_mul := by simp [mul_def, one_def]
  mul_one := by simp [mul_def, one_def]

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