single_left_injective — Mathlib

English

If b ≠ 0, then the map a ↦ single a b is injective.

Русский

Если b ≠ 0, то отображение a ↦ single a b инъективно.

LaTeX

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

Lean4

/-- `Finsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
`Finsupp.single_injective` -/
theorem single_left_injective (h : b ≠ 0) : Function.Injective fun a : α => single a b := fun _a _a' H =>
  (((single_eq_single_iff _ _ _ _).mp H).resolve_right fun hb => h hb.1).left

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