subsemiringClass — Mathlib

English

There is a CanLift instance allowing to lift membership from Set A to StarSubalgebra via the carrier map.

Русский

Существуют условия CanLift, позволяющие перенести принадлежность из множества A в StarSubalgebra через носитель.

LaTeX

$$$\\text{CanLift}(Set\\ A; StarSubalgebra\\ R A; \\text{carrier})$$$

Lean4

instance subsemiringClass : SubsemiringClass (StarSubalgebra R A) A
    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'

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