isUnit_toMatrix'_iff — Mathlib

English

An endomorphism f is invertible iff its matrix under the equivalence is invertible.

Русский

Эндоморфизм является обратимым тогда и только тогда, когда матрица этого эндоморфизма по эквивалентности обратима.

LaTeX

$$$ \\IsUnit f.toMatrix' \\iff \\IsUnit f$$$

Lean4

@[simp]
theorem isUnit_toMatrix'_iff {f : (n → R) →ₗ[R] n → R} : IsUnit f.toMatrix' ↔ IsUnit f :=
  isUnit_map_iff LinearMap.toMatrixAlgEquiv' f

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