neLocus_self_add_left

Mathlib.Data.Finsupp.NeLocus

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

English

Symmetric statement: neLocus (f + g) f = g.support.

Русский

Симметричное выражение: neLocus (f + g) f = g.support.

LaTeX

$$$ neLocus (f + g) f = g.\mathrm{support} $$$

Lean4

@[simp]
theorem neLocus_self_add_left : neLocus (f + g) f = g.support := by rw [neLocus_comm, neLocus_self_add_right]

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

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

Разделы

Аффилиация

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