toLinearMap_maxTrivLinearMapEquivLieModuleHom

English

The underlying linear map of maxTrivLinearMapEquivLieModuleHom is the original linear map f.

Русский

Понижающее линейное отображение maxTrivLinearMapEquivLieModuleHom совпадает с исходным отображением f.

LaTeX

$$$\\big(\\text{toLinearMap }(\\text{maxTrivLinearMapEquivLieModuleHom } f)\\big) = f$$$

Lean4

@[simp]
theorem toLinearMap_maxTrivLinearMapEquivLieModuleHom (f : maxTrivSubmodule R L (M →ₗ[R] N)) :
    (maxTrivLinearMapEquivLieModuleHom (M := M) (N := N) f : M →ₗ[R] N) = (f : M →ₗ[R] N) := by ext; rfl

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