of_injective — Mathlib

English

The canonical map of generators α → FreeCommRing α is injective; different symbols map to different elements.

Русский

Каноническое отображение генераторов α → FreeCommRing α инъективно; разные символы идут в различные элементы.

LaTeX

$$$ \\forall a,b,\\ \\mathrm{of}(a) = \\mathrm{of}(b) \\Rightarrow a = b $$$

Lean4

theorem of_injective : Function.Injective (of : α → FreeCommRing α) :=
  FreeAbelianGroup.of_injective.comp fun _ _ => (Multiset.coe_eq_coe.trans List.singleton_perm_singleton).mp

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