English
Let F be a type equipped with theRingInvoClass structure over a semiring R, together with an equivalence-like relation to the opposite ring. Then there is a canonical way to view any f ∈ F as a ring with involution over R, yielding a RingInvo R structure determined by f.
Русский
Пусть F — тип, оснащённый структурой RingInvoClass над полупрямым кольцом R, и существует эквивалентность до противоположного кольца. Тогда для любого элемента f ∈ F существует каноническое представление как кольца с инволюцией над R, то есть структура RingInvo R, задаваемая f.
LaTeX
$$$\mathrm{toRingInvo}(f) = (R,\, f : R \simeq R^{op},\, \text{involution}' = \mathrm{RingInvoClass.involution}(f))$$$
Lean4
/-- Turn an element of a type `F` satisfying `RingInvoClass F R` into an actual
`RingInvo`. This is declared as the default coercion from `F` to `RingInvo R`. -/
@[coe]
def toRingInvo {R} [Semiring R] [EquivLike F R Rᵐᵒᵖ] [RingInvoClass F R] (f : F) : RingInvo R :=
{ (f : R ≃+* Rᵐᵒᵖ) with involution' := RingInvoClass.involution f }
