English
For any A ∈ SL(n, R) and v ∈ R^n, the linear map associated to A, applied to v, equals Matrix.toLin'(↑A) applied to v.
Русский
Для любого A∈SL(n,R) и вектора v∈R^n линейное отображение, соответствующее A, действует на v так же, как Matrix.toLin'(↑A).
LaTeX
$$SpecialLinearGroup.toLin' (A) v = Matrix.toLin' (↑ₘA) v$$
Lean4
/-- A version of `Matrix.toLin' A` that produces linear equivalences. -/
def toLin' : SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R
where
toFun
A :=
LinearEquiv.ofLinear (Matrix.toLin' ↑ₘA) (Matrix.toLin' ↑ₘA⁻¹)
(by rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one])
(by rw [← toLin'_mul, ← coe_mul, inv_mul_cancel, coe_one, toLin'_one])
map_one' := LinearEquiv.toLinearMap_injective Matrix.toLin'_one
map_mul' A B := LinearEquiv.toLinearMap_injective <| Matrix.toLin'_mul ↑ₘA ↑ₘB
