isPairSelfAdjointSubmodule — Mathlib

English

The set of endomorphisms that are self-adjoint with respect to B and F forms a submodule of the endomorphism ring.

Русский

Множество эндоморфизмов, являющихся самосопряжёнными относительно B и F, образует подмодуль кольца эндоморфизмов.

LaTeX

$$The carrier of isPairSelfAdjointSubmodule B F is {f ∈ End_R(M) | IsPairSelfAdjoint B F f f}, closed under 0, addition, and scalar multiplication.$$

Lean4

/-- The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms. -/
def isPairSelfAdjointSubmodule : Submodule R (Module.End R M)
    where
  carrier := {f | IsPairSelfAdjoint B F f}
  zero_mem' := isAdjointPair_zero
  add_mem' hf hg := hf.add hg
  smul_mem' c _ h := h.smul c

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