instInvolutiveNeg — Mathlib

English

The negation operation on LinearPMap is involutive: applying negation twice yields the original map.

Русский

Операция отрицания на LinearPMap является инволюторной: применение отрицания дважды возвращает исходное отображение.

LaTeX

$$(-(-f)) = f$$

Lean4

instance instInvolutiveNeg : InvolutiveNeg (E →ₗ.[R] F) :=
  ⟨fun f => by
    ext x y hxy
    · rfl
    · simp only [neg_apply, neg_neg]⟩

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