carrier_neg — Mathlib

English

Let c be a conjugate-root class. Then the carrier of its negation equals the additive inverse of the carrier: the set of negatives of elements of c.carrier is exactly c.carrier with signs flipped.

Русский

Пусть c — класс сопряжённых корней. Тогда носитель его отрицания равен множеству отрицательных элементов носителя: множество −a, где a ∈ c.carrier, совпадает с носителем c.

LaTeX

$$$ \\operatorname{carrier}(-c) = -\\operatorname{carrier}(c) $$$

Lean4

@[simp]
theorem carrier_neg (c : ConjRootClass K L) : carrier (-c) = -carrier c :=
  by
  ext
  simp [mem_carrier, ← mk_neg, neg_eq_iff_eq_neg]

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