instGroupConeClass — Mathlib

English

For a commutative group G, GroupCone G carries a GroupConeClass structure, i.e., a canonical cone structure on G induces a compatible order.

Русский

Для коммутативной группы G GroupCone G образует структуру GroupConeClass, то есть каноническая конусная структура на G совместима с порядком.

LaTeX

$$$\text{GroupCone}(G)\;\Rightarrow\; \text{GroupConeClass }(\text{GroupCone }G)\; G$$$

Lean4

@[to_additive]
instance instGroupConeClass (G : Type*) [CommGroup G] : GroupConeClass (GroupCone G) G
    where
  mul_mem {C} := C.mul_mem'
  one_mem {C} := C.one_mem'
  eq_one_of_mem_of_inv_mem {C} := C.eq_one_of_mem_of_inv_mem'

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