instCoeTCOfRingInvoClass — Mathlib

English

If F carries a RingInvoClass structure over a semiring R and is equipped with an EquivLike to R, then F admits a canonical coercion to RingInvo R, i.e. F can be viewed as a RingInvo on R.

Русский

Если у F имеется структура RingInvoClass над полупрямым кольцом R и имеется эквивалентность RingInvo между F и R, то F допускает каноническое приведение к RingInvo R, то есть F можно рассматривать как кольцевую инволюцию на R.

LaTeX

$$$F\ \text{ имеет каноническое приведениe в } \mathrm{RingInvo}(R)\,.$$$

Lean4

/-- Any type satisfying `RingInvoClass` can be cast into `RingInvo` via
`RingInvoClass.toRingInvo`. -/
instance [RingInvoClass F R] : CoeTC F (RingInvo R) :=
  ⟨RingInvoClass.toRingInvo⟩

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