isUnit_toMatrix_iff — Mathlib

English

The matrix representation preserves invertibility: a linear map is invertible if and only if its matrix with respect to the basis is invertible.

Русский

Матрица представления сохраняет обратимость: линейное отображение обратимо тогда и только тогда, когда соответствующая матрица по базису обратима.

LaTeX

$$$\\IsUnit(f) \\iff \\IsUnit(\\operatorname{toMatrix}_{v_1 v_1}(f)).$$$

Lean4

@[simp]
theorem isUnit_toMatrix_iff {f : M₁ →ₗ[R] M₁} : IsUnit (f.toMatrix v₁ v₁) ↔ IsUnit f :=
  isUnit_map_iff (LinearMap.toMatrixAlgEquiv _) f

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