single_injective — Mathlib

English

The map a ↦ single a b is injective in a whenever b ≠ 0.

Русский

Карта a ↦ single a b инъективна по a при условии b ≠ 0.

LaTeX

$$$$\\text{single}_a: a \\mapsto \\text{single } a\\, b\\quad\\text{is injective if } b\\neq 0.$$$$

Lean4

/-- `Finsupp.single a b` is injective in `b`. For the statement that it is injective in `a`, see
`Finsupp.single_left_injective` -/
theorem single_injective (a : α) : Function.Injective (single a : M → α →₀ M) := fun b₁ b₂ eq =>
  by
  have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]
  rwa [single_eq_same, single_eq_same] at this

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