mem_isPairSelfAdjointSubmodule — Mathlib

English

Membership of a linear map in the pair self-adjoint submodule is equivalent to the pair self-adjointness condition.

Русский

Принадлежность линейного отображения к подмодулю парной самосопряжённости эквивалентна условию парной самосопряжённости.

LaTeX

$$f ∈ isPairSelfAdjointSubmodule B F ↔ IsPairSelfAdjoint B F f$$

Lean4

@[simp]
theorem mem_isPairSelfAdjointSubmodule (f : Module.End R M) :
    f ∈ isPairSelfAdjointSubmodule B F ↔ IsPairSelfAdjoint B F f :=
  Iff.rfl

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