ofClass — Mathlib

English

From an element s of a SubringClass S R one obtains a Subring of R whose carrier is s.

Русский

Из элемента s класса SubringClass S R получается подкольцо S в R с носителем s.

LaTeX

$$$ \\operatorname{carrier}(\\mathrm{ofClass}(s)) = s $$$

Lean4

/-- The actual `Subring` obtained from an element of a `SubringClass`. -/
@[simps]
def ofClass {S R : Type*} [Ring R] [SetLike S R] [SubringClass S R] (s : S) : Subring R
    where
  carrier := s
  add_mem' := add_mem
  zero_mem' := zero_mem _
  mul_mem' := mul_mem
  neg_mem' := neg_mem
  one_mem' := one_mem _

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