instSubringClass — Mathlib

English

Von-Neumann algebras form a subring of the algebra of bounded linear operators on H, closed under addition, multiplication, and scalar multiplication.

Русский

Алгебры Вона образуют подкольцо множества ограниченных линейных операторов на H; они замкнуты по сложению, умножению и умножению на скаляры.

LaTeX

$$$S: \\text{VonNeumannAlgebra}(H) \\Rightarrow S \\text{ is a Subring of } (H \\to\\! \\! L_{\\mathbb{C}} H).$$$

Lean4

instance instSubringClass : SubringClass (VonNeumannAlgebra H) (H →L[ℂ] H)
    where
  add_mem {s} := s.add_mem'
  mul_mem {s} := s.mul_mem'
  one_mem {s} := s.one_mem'
  zero_mem {s} := s.zero_mem'
  neg_mem {s} a ha := show -a ∈ s.toStarSubalgebra from neg_mem ha

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