ring — Mathlib

English

There is a ring structure on the space of continuous linear maps M →L[R] M with ring operations defined pointwise.

Русский

Существуют кольцевые операции на пространстве непрерывных линейных отображений M →L[R] M.

LaTeX

$$Ring (ContinuousLinearMap (RingHom.id R) M M)$$

Lean4

instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M)
    where
  __ := ContinuousLinearMap.semiring
  __ := ContinuousLinearMap.addCommGroup
  intCast z := z • (1 : M →L[R] M)
  intCast_ofNat := natCast_zsmul _
  intCast_negSucc := negSucc_zsmul _

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