ofFinsupp_injective — Mathlib

English

The embedding of finsupp into SkewMonoidAlgebra is injective, i.e., (toFinsupp) and (ofFinsupp) preserve distinctness via equivalences.

Русский

Вложение Finsupp в SkewMonoidAlgebra инъективно; различие сохраняется через эквивалентности.

LaTeX

$$$ \text{Injective}(\mathrm{ofFinsupp}) $$$

Lean4

theorem ofFinsupp_injective : Function.Injective (ofFinsupp : Finsupp _ _ → SkewMonoidAlgebra k G) := fun _ _ ↦
  congr_arg toFinsupp

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