English
The Lie algebra linear equivalence constructed from f with given inverse data g, h1, h2 is the linear equivalence whose toLinearMap is f and whose invFun, left_inv, right_inv are g, h1, h2 respectively.
Русский
Гомотия Ли-алгебр, построенная из f с данными обратности g, h1, h2, равна линейному эквиваленту, у которого toLinearMap = f, invFun = g, left_inv = h1, right_inv = h2.
LaTeX
$$$ (\mathrm{mk}(f,g,h_1,h_2) : L_1 \simeq_R L_2) = { f\, with\, invFun := g\, ,\, left_inv := h_1\, ,\, right_inv := h_2 } $$$
Lean4
@[simp]
theorem toLinearEquiv_mk (f : L₁ →ₗ⁅R⁆ L₂) (g h₁ h₂) :
(mk f g h₁ h₂ : L₁ ≃ₗ[R] L₂) =
{ f with
invFun := g
left_inv := h₁
right_inv := h₂ } :=
rfl
