Theorems · Theorem · group theory

FixedDetMatrices.reduce.eq_def

∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m),
  FixedDetMatrices.reduce A =
    if ↑A 1 0 = 0 then
      if 0 < ↑A 0 0 then ModularGroup.T ^ (-(↑A 0 1 / ↑A 1 1)) • A
      else ModularGroup.T ^ (-(-↑A 0 1 / -↑A 1 1)) • ModularGroup.S • ModularGroup.S • A
    else FixedDetMatrices.reduce (FixedDetMatrices.reduceStep A)

Defined in

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Cited by

0 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound