add_eq_zero_iff

Mathlib.Data.DFinsupp.Order

URI: https://scilib.ai/kg/mathlib#DFinsupp.add_eq_zero_iff

English

For f,g in DFinsupp fun i => α_i, the sum f+g equals zero if and only if f and g are both zero.

Русский

Для элементов f,g пространства DFinsupp fun i => α_i сумма f+g равна нулю тогда и только тогда, когда f = 0 и g = 0.

LaTeX

$$$f+g=0 \\iff f=0 \\land g=0$$$

Lean4

@[simp]
theorem add_eq_zero_iff (f g : Π₀ i, α i) : f + g = 0 ↔ f = 0 ∧ g = 0 := by simp [DFunLike.ext_iff, forall_and]

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

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

Разделы

Аффилиация

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