English
For a coprime pair p=(c0,c1) there is a real-linear isomorphism lcRow0Extend(p) that sends a matrix [[a,b],[c,d]] to [[ac0+bd0, -ad0+bc0],[c,d]] where (c0,d0) are fixed by p.
Русский
Для взаимно простого p=(c0,c1) существует линейное изоморфизм lcRow0Extend(p), переводящий матрицу [[a,b],[c,d]] в [[ac0+bd0, -ad0+bc0],[c,d]].
LaTeX
$$$lcRow0Extend(p): M_{2}(\\mathbb{R}) \\to M_{2}(\\mathbb{R})\\;\\\\ \\text{ defined by }\\; \n[[a,b],[c,d]]\\mapsto [[a c_0 + b d_0, -a d_0 + b c_0],[c,d]],$ where p=(c_0,d_0).$$$
Lean4
/-- Linear map sending the matrix [a, b; c, d] to the matrix [ac₀ + bd₀, - ad₀ + bc₀; c, d], for
some fixed `(c₀, d₀)`. -/
@[simps!]
def lcRow0Extend {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
Matrix (Fin 2) (Fin 2) ℝ ≃ₗ[ℝ] Matrix (Fin 2) (Fin 2) ℝ :=
LinearEquiv.piCongrRight
![by
refine
LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
(GeneralLinearGroup.toLin (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) ?_))
norm_cast
rw [neg_sq]
exact hcd.sq_add_sq_ne_zero, LinearEquiv.refl ℝ (Fin 2 → ℝ)]
