unique_single_eq_iff — Mathlib

English

In a Unique α, for any a,a' and b,b', single a b = single a' b' iff b = b'.

Русский

В уникальном α равносильно: для любых a,a' и b,b' верно, что single a b = single a' b' тогда и только тогда, когда b = b'.

LaTeX

$$$\mathrm{single}(a,b) = \mathrm{single}(a',b') \iff b = b'$$$

Lean4

@[simp]
theorem unique_single_eq_iff [Unique α] {b' : M} : single a b = single a' b' ↔ b = b' := by
  rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same, single_eq_same]

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