single_injective — Mathlib

English

For each a ∈ G, the map b ↦ single a b is injective from k to SkewMonoidAlgebra k G.

Русский

Для каждого a ∈ G отображение b ↦ single a b инъективно из k в SkewMonoidAlgebra k G.

LaTeX

$$$\\text{single}_a : k \\to \\ SkewMonoidAlgebra\\ k\\ G\\ is\\ injective$$$

Lean4

theorem single_injective (a : G) : Function.Injective (single a : k → SkewMonoidAlgebra k G) :=
  toFinsuppAddEquiv.symm.injective.comp (Finsupp.single_injective a)

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