instRingInvoClass — Mathlib

English

The RingInvo R carries a RingInvoClass structure, i.e., the RingInvo objects on R form a class with the operations map_add, map_mul and an involution.

Русский

К кольцевой инволюции R приписывается структура RingInvoClass, то есть у RingInvo R образуется класс с операциями сложения и умножения и инволюцией.

LaTeX

$$$\text{RingInvo}(R) \text{ carries a } \mathrm{RingInvoClass} \text{ structure: }\ map\_add,\ map\_mul,\ involution'. $$$

Lean4

instance : RingInvoClass (RingInvo R) R where
  map_add f := f.map_add'
  map_mul f := f.map_mul'
  involution f := f.involution'

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