reduce_rec

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

URI: https://scilib.ai/kg/mathlib#FixedDetMatrices.reduce_rec

Lean4

/-- Reduction lemma for integral FixedDetMatrices. -/
@[elab_as_elim]
def reduce_rec {C : Δ m → Sort*} (base : ∀ A : Δ m, (A.1 1 0) = 0 → C A)
    (step : ∀ A : Δ m, (A.1 1 0) ≠ 0 → C (reduceStep A) → C A) : ∀ A, C A := fun A =>
  by
  by_cases h : (A.1 1 0) = 0
  · exact base _ h
  · exact step A h (reduce_rec base step (reduceStep A))
termination_by A => Int.natAbs (A.1 1 0)
decreasing_by
  zify
  exact reduce_aux h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru