toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm

English

The symmetric version of the underlying linear map of maxTrivLinearMapEquivLieModuleHom coincides with the symmetric map.

Русский

Симметричная версия линейного отображения maxTrivLinearMapEquivLieModuleHom совпадает с симметричным отображением.

LaTeX

$$$\\text{toLinearMap}_{\\text{symm}}(\\maxTrivLinearMapEquivLieModuleHom) = \\text{toLinearMap}(\\text{symm})$$$

Lean4

@[simp]
theorem toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm (f : M →ₗ⁅R,L⁆ N) :
    (maxTrivLinearMapEquivLieModuleHom (M := M) (N := N) |>.symm f : M →ₗ[R] N) = (f : M →ₗ[R] N) :=
  rfl

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