Theorems · Definition · group theory

FixedDetMatrices.reduce_rec

{m : ℤ} →
  {C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3} →
    ((A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A) →
      ((A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (FixedDetMatrices.reduceStep A) → C A) →
        (A : FixedDetMatrix (Fin 2) ℤ m) → C A

Reduction lemma for integral FixedDetMatrices.

Defined in

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Cited by

3 results in Mathlib

Foundations

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