coe_T_zpow — Mathlib

English

Re-statement: For any A ∈ SL(2,R) and j, the pair (A(0,j), A(1,j)) is coprime.

Русский

Повтор: для любого A ∈ SL(2,R) и j, пара (A(0,j), A(1,j)) взаимно простая.

LaTeX

$$IsCoprime (A.0 j) (A.1 j)$$

Lean4

theorem coe_T_zpow (n : ℤ) : (T ^ n).1 = !![1, n; 0, 1] := by
  induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring

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