English
There is a canonical CoeFun structure identifying GL⁺(2,ℝ) with its natural action on the coordinate representation of vectors, i.e., each g acts by the standard matrix multiplication on ℝ^2 via its coordinate functions.
Русский
Существует каноническая структура CoeFun, устанавливающая GL⁺(2,ℝ) как естественное действие на координатном представлении вектора, то есть каждую матрицу g действует на ℝ^2 обычным умножением на вектор.
LaTeX
$$$$ g \\mapsto (v \\mapsto g v) \\quad \\text{for } g \\in GL^{+}(2,\\mathbb{R}). $$$$
Lean4
theorem isometry_pos_mul (a : { x : ℝ // 0 < x }) : Isometry (a • · : ℍ → ℍ) :=
by
refine Isometry.of_dist_eq fun y₁ y₂ => ?_
simp only [dist_eq, coe_pos_real_smul, pos_real_im]; congr 2
rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs, Real.norm_eq_abs,
mul_left_comm]
exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')
