English
A non-unital k-algebra homomorphism from SkewMonoidAlgebra k G to A is uniquely determined by its values on the functions single x 1 (for x in G).
Русский
Нелинейный (негомоморфизм, не единичной единицы) k-алгеброморфизм из SkewMonoidAlgebra k G в A определяется единственным образом по значениям на функции single x 1 (для x из G).
LaTeX
$$$\forall \phi_1, \phi_2:\ SkewMonoidAlgebra k G \to_{n\_a} A,\ (\forall x,\ \phi_1( single x 1) = \phi_2(single x 1)) \Rightarrow \phi_1 = \phi_2$$$
Lean4
/-- `single` as a `DistribMulActionSemiHom`.
See also `lsingle` for the version as a linear map. -/
@[simps]
def single [DistribMulAction R M] {α : Type*} (a : α) : M →+[R] SkewMonoidAlgebra M α
where
__ := singleAddHom a
map_smul' k m := by simp [singleAddHom, smul_single, MonoidHom.id_apply]
