mem_skewAdjointSubmodule — Mathlib

English

Membership in the skew-adjoint submodule is equivalent to being skew-adjoint with respect to B.

Русский

Принадлежность к подмодулю косо‑самосопряжённых эквивалентна кососопряжённости по B.

LaTeX

$$f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint f$$

Lean4

@[simp]
theorem mem_skewAdjointSubmodule (f : Module.End R M) : f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint f :=
  by
  rw [isSkewAdjoint_iff_neg_self_adjoint]
  exact Iff.rfl

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