of_injective — Mathlib

English

Let k be a nontrivial semiring and G a monoid with a compatible action on k. Then the canonical embedding of the monoid algebra into the skew monoid algebra, given by of k G, is injective.

Русский

Пусть k — ненулевая полугруппа, G — моноид, на k задано совместное действие моноида G. Тогда каноническое отображение of k G в SkewMonoidAlgebra k G инъективно.

LaTeX

$$$\forall a,b\in G,\; of\ k\,G\,a = of\ k\,G\,b \Rightarrow a = b$$$

Lean4

theorem of_injective [Nontrivial k] : Function.Injective (of k G) := fun a b h ↦
  by
  simp_rw [of_apply, ← toFinsupp_inj] at h
  simpa using (Finsupp.single_eq_single_iff _ _ _ _).mp h

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