single_left_inj

Mathlib.Data.Finsupp.Single

URI: https://scilib.ai/kg/mathlib#Finsupp.single_left_inj

English

If b ≠ 0, then single a b = single a' b iff a = a'.

Русский

Если b ≠ 0, то single a b = single a' b тогда и только тогда, когда a = a'.

LaTeX

$$$$\\text{If } b \\neq 0: \\quad \\text{single } a\\, b = \\text{single } a'\\, b \\iff a = a'.$$$$

Lean4

theorem single_left_inj (h : b ≠ 0) : single a b = single a' b ↔ a = a' :=
  (single_left_injective h).eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru