toAddEquivClass — Mathlib

English

The underlying function of the constructed ring equivalence is exactly the given function e.

Русский

Функция, лежащая в основе сконструированного кольцевого эквивалента, равна заданной функции e.

LaTeX

$$\mathrm{coe}(\langle e, h_3, h_4 \rangle) = e$$

Lean4

instance (priority := 100) toAddEquivClass [Mul R] [Add R] [Mul S] [Add S] [h : RingEquivClass F R S] :
    AddEquivClass F R S :=
  { h with }
    -- See note [lower instance priority]

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