toFinsupp_injective — Mathlib

English

The map toFinsupp: SkewMonoidAlgebra k G → Finsupp _ _ is injective; i.e., if f.toFinsupp = g.toFinsupp then f = g.

Русский

Отображение toFinsupp: SkewMonoidAlgebra k G → Finsupp _ _ инъективно; то есть f.toFinsupp = g.toFinsupp ⇒ f = g.

LaTeX

$$$ \forall f,g \in SkewMonoidAlgebra(k,G),\; f^{\mathrm{toFinsupp}} = g^{\mathrm{toFinsupp}} \Rightarrow f = g $$$

Lean4

theorem toFinsupp_injective : Function.Injective (toFinsupp : SkewMonoidAlgebra k G → Finsupp _ _) := fun ⟨_⟩ _ ↦
  congr_arg _

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