coeFn_generalLinearEquiv — Mathlib

English

For any f in GeneralLinearGroup R M, the canonical representative of the associated linear map equals the image of f under generalLinearEquiv, i.e., (generalLinearEquiv R M f) = (f : M → M).

Русский

Для любого f ∈ GeneralLinearGroup R M канонический представитель соответствующего линейного отображения равен изображению f через generalLinearEquiv: (generalLinearEquiv R M f) = (f : M → M).

LaTeX

$$$ (generalLinearEquiv R M f) = (f : M \to M). $$$

Lean4

@[simp]
theorem coeFn_generalLinearEquiv (f : GeneralLinearGroup R M) : (generalLinearEquiv R M f) = (f : M → M) :=
  rfl

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