neLocus_self_add_right — Mathlib

English

The neLocus of f1 − g and f2 − g equals the neLocus of f1 and f2: neLocus (f1 − g) (f2 − g) = f1.neLocus f2.

Русский

Локус вычитания справа равен локусу левых аргументов.

LaTeX

$$$ \mathrm{neLocus} (f_1 - g) (f_2 - g) = f_1.\mathrm{neLocus} f_2 $$$

Lean4

@[simp]
theorem neLocus_self_add_right : neLocus f (f + g) = g.support := by
  rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]

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