coe_mk — Mathlib

English

If AbsoluteValue.mk is built from a function f with supporting data, then the resulting absolute value has the underlying map equal to f.

Русский

Если конструктор AbsoluteValue.mk построен из отображения f с дополнительными данными, то полученное абсолютное значение имеет отображение, равное f.

LaTeX

$$$\big( AbsoluteValue.mk(f,h_1,h_2,h_3)\;:\; R\to S\big)=f$$$

Lean4

@[simp]
theorem coe_mk (f : R →ₙ* S) {h₁ h₂ h₃} : (AbsoluteValue.mk f h₁ h₂ h₃ : R → S) = f :=
  rfl

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