single_one_mul_apply — Mathlib

English

If R is nontrivial, the embedding of M into MonoidAlgebra R M is injective: if of_R_M(m) = of_R_M(n) then m = n.

Русский

Если R непривередливое, вложение M в MonoidAlgebra R M инъективно: из of_R_M(m) = of_R_M(n) следует m = n.

LaTeX

$$$\forall m,n \in M: \operatorname{of}(m) = \operatorname{of}(n) \Rightarrow m = n$ (при $R$ ненулевом)$$

Lean4

@[to_additive (dont_translate := R) single_zero_mul_apply]
theorem single_one_mul_apply (x : MonoidAlgebra R M) (r : R) (m : M) :
    (single 1 r * x : MonoidAlgebra R M) m = r * x m :=
  x.single_mul_apply_aux (by simp)

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