add_left_inj

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.add_left_inj

English

s + u = t + u iff s = t.

Русский

s + u = t + u тогда и только тогда, когда s = t.

LaTeX

$$$s + u = t + u \iff s = t$$$

Lean4

protected theorem add_left_inj : s + u = t + u ↔ s = t := by classical simp [Multiset.ext]

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

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

Разделы

Аффилиация

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