coe_mk — Mathlib

English

The underlying map of the constructed Lie module equivalence is f; that is, the function component of the equivalence is exactly f.

Русский

У отображения, полученного конструктором эквивалентности Ли-модуля, как функция, подстановка равна f; то есть базовая функция равна f.

LaTeX

$$$\\bigl((\\langle f, invFun, h_1, h_2 \\rangle) : M \\to N\\bigr) = f$$$

Lean4

@[simp]
theorem coe_mk (f : M →ₗ⁅R,L⁆ N) (invFun h₁ h₂) : ((⟨f, invFun, h₁, h₂⟩ : M ≃ₗ⁅R,L⁆ N) : M → N) = f :=
  rfl

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