coe_mk — Mathlib

English

The coercion of the constructed ring equivalence from its constructor equals the underlying function e.

Русский

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

LaTeX

$$coe_mk (e h3 h4) : ⇑(⟨e, h3, h4⟩ : R ≃+* S) = e$$

Lean4

@[simp]
theorem coe_mk (e h₃ h₄) : ⇑(⟨e, h₃, h₄⟩ : R ≃+* S) = e :=
  rfl

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