reduce — Mathlib

English

The reduction map moves Δ m toward a canonical representative by alternating steps with S and T.

Русский

Редукция продвигает Δ m к каноническому представителю, чередуя шаги S и T.

LaTeX

$$$reduce: Δ m \to Δ m$, defined recursively by cases using reduceStep and the generators S,T.$$

Lean4

/-- Map from `Δ m → Δ m` which reduces a `FixedDetMatrix` towards a representative element
in reps -/
def reduce : Δ m → Δ m := fun A ↦
  if (A.1 1 0) = 0 then
    if 0 < A.1 0 0 then (T ^ (-(A.1 0 1 / A.1 1 1))) • A
    else
      (T ^ (-(-A.1 0 1 / -A.1 1 1))) •
        (S • (S • A)) --the -/- don't cancel with ℤ divs.

  else reduce (reduceStep A)
termination_by b => Int.natAbs (b.1 1 0)
decreasing_by
  next a h =>
    zify
    exact reduce_aux h

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