singleOneRingHom — Mathlib

English

There is a RingHom from R to MonoidAlgebra R M sending r to the element single 1 r, i.e., the unit coefficient at the unit basis element.

Русский

Существует кольцевой гомоморфизм от R к MonoidAlgebra R M, отправляющий r в элемент single 1 r.

LaTeX

$$$\operatorname{singleOneRingHom} : R \to+* MonoidAlgebra\; R\; M$, $\operatorname{toFun}(r) = \operatorname{single}(1_M, r)$$$

Lean4

/-- `MonoidAlgebra.single 1` as a `RingHom` -/
@[to_additive (attr := simps) (dont_translate := R) /-- `AddMonoidAlgebra.single 1` as a `RingHom` -/
    ]
def singleOneRingHom : R →+* MonoidAlgebra R M :=
  { singleAddHom 1 with
    toFun := single 1
    map_one' := rfl
    map_mul' := fun x y => by simp }

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