English
For A ∈ unitaryGroup(n, α), toLinearEquiv(A) is a linear equivalence between α^n and α^n given by left multiplication by A, with inverse given by A⁻¹.
Русский
Для A ∈ unitaryGroup(n, α) toLinearEquiv(A) задаёт линейное биекование между α^n и α^n, равное умножению слева на A, с обратным отображением A⁻¹.
LaTeX
$$toLinearEquiv(A) : (n → α) ≃ₗ[α] (n → α) with left_inv and right_inv as in the definition.$$
Lean4
/-- `Matrix.unitaryGroup.toLinearEquiv A` is matrix multiplication of vectors by `A`, as a linear
equivalence. -/
def toLinearEquiv (A : unitaryGroup n α) : (n → α) ≃ₗ[α] n → α :=
{ Matrix.toLin' A.1 with
invFun := toLin' A⁻¹
left_inv := fun x =>
calc
(toLin' A⁻¹).comp (toLin' A) x = (toLin' (A⁻¹ * A)) x := by rw [← toLin'_mul]
_ = x := by rw [inv_mul_cancel, toLin'_one, id_apply]
right_inv := fun x =>
calc
(toLin' A).comp (toLin' A⁻¹) x = toLin' (A * A⁻¹) x := by rw [← toLin'_mul]
_ = x := by rw [mul_inv_cancel, toLin'_one, id_apply] }
