English
Given p = (c,d) ∈ ℤ^2, there is a real-linear functional on 2×2 matrices that sends a matrix [[a,b],[*,*]] to a c + b d, i.e., the map A ↦ a c + b d.
Русский
Пусть p=(c,d)∈ℤ^2. Существует реальное линейное отображение, которое сопоставляет матрице [[a,b],[*,*]] выражение a c + b d.
LaTeX
$$$\\text{For } p=(c,d)\\in \\mathbb{Z}^2,\\; A=(a_{ij}) \\in M_{2}(\\mathbb{R}):\\ lcRow0(p)(A)=a_{11}c + a_{12}d.$$$
Lean4
/-- Given `coprime_pair` `p=(c,d)`, the matrix `[[a,b],[*,*]]` is sent to `a*c+b*d`.
This is the linear map version of this operation.
-/
def lcRow0 (p : Fin 2 → ℤ) : Matrix (Fin 2) (Fin 2) ℝ →ₗ[ℝ] ℝ :=
((p 0 : ℝ) • LinearMap.proj (0 : Fin 2) + (p 1 : ℝ) • LinearMap.proj (1 : Fin 2) : (Fin 2 → ℝ) →ₗ[ℝ] ℝ).comp
(LinearMap.proj 0)
