mulVecSL — Mathlib

English

Multiplying a coprime vector on the left by an SL(2,R) matrix preserves coprimality of its coordinates.

Русский

Умножение вектора с взаимной простотой слева на матрицу SL(2,R) сохраняет взаимную простоту координат.

LaTeX

$$IsCoprime ((A.val.mulVec v) 0) ((A.val.mulVec v) 1)$$

Lean4

/-- A vector with coprime entries, left-multiplied by a matrix in `SL(2, R)`, has
coprime entries. -/
theorem mulVecSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
    IsCoprime ((A.1 *ᵥ v) 0) ((A.1 *ᵥ v) 1) := by simpa only [← vecMul_transpose] using hab.vecMulSL A.transpose

Похожие утверждения