g_eq_of_c_eq_one — Mathlib

English

If c = 1, then g equals T^{g00} S T^{g11}, i.e., it factors through T and the standard S-move.

Русский

Если c = 1, то g = T^{g00} S T^{g11}, то есть разложение через T и S.

LaTeX

$$$\\text{If } g_{1,0} = 1,\\; g = T^{g_{0,0}}\, S\, T^{g_{1,1}}.$$$

Lean4

theorem g_eq_of_c_eq_one (hc : g 1 0 = 1) : g = T ^ g 0 0 * S * T ^ g 1 1 :=
  by
  have hg := g.det_coe.symm
  replace hg : g 0 1 = g 0 0 * g 1 1 - 1 := by rw [det_fin_two, hc] at hg; omega
  refine Subtype.ext ?_
  conv_lhs => rw [(g : Matrix _ _ ℤ).eta_fin_two]
  simp only [hg, sub_eq_add_neg, hc, coe_mul, coe_T_zpow, coe_S, mul_fin_two, mul_zero, mul_one, zero_add, one_mul,
    add_zero, zero_mul]

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