reduce_of_not_pos — Mathlib

English

If A satisfies A_{10} ≈ 0 and A_{11} ≤ 0 (not positive), then reduce A equals a conjugate by S,S of A times T move, etc.

Русский

Если A_{10} ≈ 0 и A_{11} ≤ 0 (не положительно), то редукция A равна действию S•S•A с дополнительной T-комбинацией.

LaTeX

$$$A_{10}=0 \land A_{11} \le 0 \Rightarrow reduce(A) = T^{-( -A_{01}/-A_{11})} \cdot (S \cdot (S \cdot A)).$$$

Lean4

theorem reduce_of_not_pos {A : Δ m} (hc : (A.1 1 0) = 0) (ha : ¬0 < A.1 0 0) :
    reduce A = (T ^ (-(-A.1 0 1 / -A.1 1 1))) • (S • (S • A)) :=
  by
  rw [reduce]
  simp only [zpow_neg, Int.ediv_neg, neg_neg] at *
  simp_rw [if_pos hc, if_neg ha]

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