neg_mem — Mathlib

English

The set of symplectic matrices is closed under taking additive inverses: if A is symplectic, then -A is also symplectic.

Русский

Множество симплектических матриц замкнуто относительно противоположной операции: если A симплектическая, то и -A симплектическая.

LaTeX

$$A ∈ Sp(l,R) ⇒ -A ∈ Sp(l,R)$$

Lean4

theorem neg_mem (h : A ∈ symplecticGroup l R) : -A ∈ symplecticGroup l R :=
  by
  rw [mem_iff] at h ⊢
  simp [h]

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