selfAdjointSubmodule — Mathlib

English

The set of self-adjoint endomorphisms (with respect to B) forms a submodule of End_R(M).

Русский

Множество самосопряжённых эндоморфизмов образует подмодуль End_R(M).

LaTeX

$$The submodule is the collection { f ∈ End_R(M) | IsSelfAdjoint_BF f f } for fixed B,F, i.e., { f ∈ End_R(M) | IsPairSelfAdjoint B F f f }.$$

Lean4

/-- The set of self-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact
it is a Jordan subalgebra.) -/
def selfAdjointSubmodule :=
  isPairSelfAdjointSubmodule B B

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