isUnit_toLin_iff — Mathlib

English

For the FinTwoProd basis, the linear map corresponding to a 2×2 matrix acts on a pair by the standard linear combination: the first component is a x1 + b x2, the second is c x1 + d x2.

Русский

Отображение 2×2 над Basis.finTwoProd действует на пару $(x_1,x_2)$ как $(a x_1 + b x_2,\; c x_1 + d x_2)$.

LaTeX

$$$\\text{Matrix.toLin} (Basis.finTwoProd R) (Basis.finTwoProd R) \\!\\![][a,b;c,d] (x,y) = (a x + b y,\; c x + d y).$$$

Lean4

@[simp]
theorem isUnit_toLin_iff {M : Matrix n n R} : IsUnit (M.toLin v₁ v₁) ↔ IsUnit M :=
  isUnit_map_iff (LinearMap.toMatrixAlgEquiv _).symm M

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