of_injective — Mathlib

English

The canonical map of α into FreeGroup α is injective.

Русский

Каноническое отображение α в FreeGroup α инъективно.

LaTeX

$$$\\text{of}: \\alpha \\to FreeGroup(\\alpha)$ is injective.$$

Lean4

/-- The canonical map from the type to the free group is an injection. -/
@[to_additive /-- The canonical map from the type to the additive free group is an injection. -/
    ]
theorem of_injective : Function.Injective (@of α) := fun _ _ H =>
  by
  let ⟨L₁, hx, hy⟩ := Red.exact.1 H
  simp [Red.singleton_iff] at hx hy; simp_all

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