instRingConeClass — Mathlib

English

The collection of RingCones on a ring R forms a RingConeClass, i.e., RingCone R can be equipped with a class of subcone structures compatible with the ring operations.

Русский

Коллекция RingCones на кольце R образует RingConeClass, то есть RingCone R можно оснастить классом подконусов, совместимым с операциями кольца.

LaTeX

$$$ \\forall R\\ [\\text{Ring } R],\\; \\text{RingConeClass}(\\text{RingCone}(R),R). $$$

Lean4

instance instRingConeClass (R : Type*) [Ring R] : RingConeClass (RingCone R) R
    where
  add_mem {C} := C.add_mem'
  zero_mem {C} := C.zero_mem'
  mul_mem {C} := C.mul_mem'
  one_mem {C} := C.one_mem'
  eq_zero_of_mem_of_neg_mem {C} := C.eq_zero_of_mem_of_neg_mem'

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